src/Tools/interpretation_with_defs.ML
Wed, 19 Feb 2014 22:05:15 +0100 haftmann more convenient syntax for permanent interpretation
Wed, 19 Feb 2014 22:05:05 +0100 haftmann aggiornamento for "interpretation with definitions": operate uniformly on theory and locale level under the brand of "permanent interpretation"
Sun, 01 Apr 2012 19:07:32 +0200 wenzelm added Attrib.global_notes/local_notes/generic_notes convenience;
Fri, 16 Mar 2012 18:20:12 +0100 wenzelm outer syntax command definitions based on formal command_spec derived from theory header declarations;
Thu, 15 Mar 2012 20:07:00 +0100 wenzelm prefer formally checked @{keyword} parser;
Thu, 15 Mar 2012 19:02:34 +0100 wenzelm declare minor keywords via theory header;
Tue, 13 Mar 2012 20:04:24 +0100 wenzelm more explicit indication of def names;
Sat, 10 Mar 2012 20:02:15 +0100 wenzelm tuned;
Fri, 28 Oct 2011 17:15:52 +0200 wenzelm tuned signature -- refined terminology;
Sat, 16 Apr 2011 16:15:37 +0200 wenzelm modernized structure Proof_Context;
Sat, 15 Jan 2011 20:05:29 +0100 haftmann experimental variant of interpretation with simultaneous definitions, plus example
less more (0) tip