src/FOL/ex/LocaleTest.thy
Tue, 16 Sep 2008 12:26:15 +0200 ballarin No interpretation of locale with dangling type frees.
Tue, 02 Sep 2008 17:31:20 +0200 ballarin Interpretation commands no longer accept interpretation attributes.
Wed, 06 Aug 2008 16:41:40 +0200 ballarin Interpretation command (theory/proof context) no longer simplifies goal.
Mon, 04 Aug 2008 10:37:33 +0200 ballarin Updated locale tests.
Fri, 25 Jul 2008 12:03:32 +0200 haftmann dropped locale (open)
Wed, 16 Jul 2008 14:21:57 +0200 ballarin Removed uses of context element includes.
Mon, 14 Apr 2008 17:54:56 +0200 ballarin Changed naming scheme for theorems generated by interpretations.
Thu, 20 Mar 2008 00:20:44 +0100 wenzelm simplified get_thm(s): back to plain name argument;
Wed, 19 Mar 2008 22:27:57 +0100 wenzelm renamed datatype thmref to Facts.ref, tuned interfaces;
Wed, 05 Mar 2008 21:24:03 +0100 wenzelm explicit referencing of background facts;
Mon, 05 Nov 2007 17:47:52 +0100 ballarin Tests enforce proper export behaviour.
Mon, 01 Oct 2007 12:24:45 +0200 ballarin unfold_locales workaround
Fri, 31 Aug 2007 18:46:33 +0200 wenzelm do not touch quick_and_dirty;
Mon, 23 Jul 2007 13:48:30 +0200 ballarin interpretation: equations are propositions not pairs of terms;
Fri, 11 May 2007 00:43:45 +0200 wenzelm tuned proofs;
Fri, 20 Apr 2007 16:55:38 +0200 ballarin Interpretation equations applied to attributes
Fri, 13 Apr 2007 10:02:30 +0200 ballarin Experimental code for the interpretation of definitions.
Mon, 04 Sep 2006 15:27:30 +0200 ballarin More locale test code.
Fri, 07 Jul 2006 09:24:05 +0200 ballarin Modified comment.
Tue, 04 Jul 2006 14:47:01 +0200 ballarin Method intro_locales replaced by intro_locales and unfold_locales.
Tue, 20 Jun 2006 15:53:44 +0200 ballarin Restructured locales with predicates: import is now an interpretation.
Tue, 06 Jun 2006 10:05:57 +0200 ballarin Improved parameter management of locales.
Fri, 16 Sep 2005 14:44:52 +0200 ballarin tuned
Fri, 02 Sep 2005 09:50:58 +0200 ballarin print_locale omits facts by default
Wed, 24 Aug 2005 12:07:00 +0200 ballarin Printing of interpretations: option to show witness theorems;
Wed, 17 Aug 2005 17:04:15 +0200 ballarin Improved generation of witnesses in interpretation.
Mon, 08 Aug 2005 22:11:31 +0200 ballarin Release of interpretation in locale.
Tue, 02 Aug 2005 16:52:21 +0200 ballarin First version of interpretation in locales. Not yet fully functional.
Thu, 07 Jul 2005 15:52:31 +0200 ballarin Preparations for interpretation of locales in locales.
Thu, 30 Jun 2005 14:06:29 +0200 ballarin Proper treatment of beta-redexes in witness theorems.
Wed, 08 Jun 2005 16:11:09 +0200 ballarin Fixed "axiom" generation for mixed locales with and without predicates.
Wed, 01 Jun 2005 12:30:49 +0200 ballarin Locales: new element constrains, parameter renaming with syntax,
Fri, 27 May 2005 16:24:48 +0200 ballarin Locale expressions: rename with optional mixfix syntax.
Mon, 25 Apr 2005 17:58:41 +0200 ballarin Subsumption of locale interpretations.
Mon, 18 Apr 2005 09:25:23 +0200 ballarin Interpretation supports statically scoped attributes; documentation.
Mon, 11 Apr 2005 12:34:34 +0200 ballarin First release of interpretation commands.
Thu, 24 Mar 2005 17:03:37 +0100 ballarin Further work on interpretation commands. New command `interpret' for
Thu, 10 Mar 2005 17:48:36 +0100 ballarin Registrations of global locale interpretations: improved, better naming.
Wed, 09 Mar 2005 18:44:52 +0100 ballarin First version of global registration command.
less more (0) tip