src/FOL/ex/LocaleTest.thy
Wed, 11 Nov 2009 21:53:58 +0100 ballarin Enables tests for locale functionality that is now available.
Wed, 04 Nov 2009 22:51:27 +0100 ballarin Use PrintMode.setmp to make thread-safe; avoid code clones.
Mon, 02 Nov 2009 22:51:22 +0100 ballarin Make output indenpendent of current print mode.
Mon, 02 Nov 2009 21:27:26 +0100 ballarin Relax on type agreement with original context when applying term syntax.
Sat, 26 Sep 2009 21:03:57 +0200 ballarin Stricter test: raise error if registration generates duplicate theorem.
Sat, 28 Mar 2009 00:13:01 +0100 ballarin Merged.
Fri, 27 Mar 2009 20:25:07 +0100 ballarin Comments updated.
Thu, 26 Mar 2009 20:08:55 +0100 wenzelm interpretation/interpret: prefixes are mandatory by default;
Fri, 16 Jan 2009 15:14:16 +0100 haftmann adapted to changes in class package
Thu, 15 Jan 2009 14:52:23 +0100 haftmann decativate Toplevel.debug after reading
Mon, 05 Jan 2009 15:35:42 +0100 haftmann removed locale adaption layer
Thu, 16 Oct 2008 17:19:47 +0200 ballarin More occurrences of 'includes' gone.
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