[isabelle-dev] Additional type variable(s) in specification
florian.haftmann at informatik.tu-muenchen.de
Fri Dec 3 08:02:44 CET 2010
> 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
-------------- next part --------------
A non-text attachment was scrubbed...
Size: 262 bytes
Desc: OpenPGP digital signature
More information about the isabelle-dev