[isabelle-dev] Additional type variable(s) in specification

[Florian Haftmann]

> I think there is a formal difference here that is beyond "Isar" vs. "ML":
> 
> a) If function calls inductive, then it is exclusively interested in
> getting an inhabitant of a specification in the auxiliary context (which
> I nowadays prefer to call the "package context"). Its interpretation in
> the target is really arbitrary. Local_Theory.define does this uniformly.
> 
> b) A user invocation of inductive via the Isar command does not care
> about the package context, which is discarded immediately. Here the
> target is what counts. In particular, the image in the target is very
> irregular at the moment, since the type arguments are only inserted in
> very special situations.

I agree that the distinction between a) »foundation mode« and b)
»specification mode« is critical.  When the whole issue was brought up
at a certain situation in 2009 (or 2008), my first idea was to this
distinction could be put into the binding, i.e. bindings what have a
»foundation flag« which by default is off (e.g. for bindings from the
theory text) but can be set by packages internally (e.g. when function
invokes inductive).

	Florian

-- 

Home:
http://www.in.tum.de/~haftmann

PGP available:
http://home.informatik.tu-muenchen.de/haftmann/pgp/florian_haftmann_at_informatik_tu_muenchen_de

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 262 bytes
Desc: OpenPGP digital signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20101203/e584acf0/attachment.sig>