> 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
signature.asc
Description: OpenPGP digital signature
_______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
