| Mon, 24 May 2010 10:48:32 +0200 |
ballarin |
Reapply mixin patch: base for performance improvements.
|
file |
diff |
annotate
|
| Fri, 14 May 2010 21:23:29 +0200 |
ballarin |
Revert mixin patch due to inacceptable performance drop.
|
file |
diff |
annotate
|
| Thu, 13 May 2010 13:30:16 +0200 |
ballarin |
Add mixin to base morphism, required by class package; cf ab324ffd6f3d.
|
file |
diff |
annotate
|
| Thu, 11 Feb 2010 21:00:36 +0100 |
ballarin |
A rough implementation of full mixin inheritance; additional unit tests.
|
file |
diff |
annotate
|
| Mon, 01 Feb 2010 21:59:27 +0100 |
ballarin |
More mixin tests.
|
file |
diff |
annotate
|
| Sat, 21 Nov 2009 17:39:54 +0100 |
ballarin |
Removed obsolete comment.
|
file |
diff |
annotate
|
| Sat, 21 Nov 2009 17:37:07 +0100 |
ballarin |
Merged.
|
file |
diff |
annotate
|
| Sat, 21 Nov 2009 17:35:55 +0100 |
ballarin |
More tests for locale interpretation.
|
file |
diff |
annotate
|
| Fri, 13 Nov 2009 21:11:15 +0100 |
wenzelm |
modernized structure Local_Theory;
|
file |
diff |
annotate
|
| Wed, 11 Nov 2009 21:53:58 +0100 |
ballarin |
Enables tests for locale functionality that is now available.
|
file |
diff |
annotate
|
| Wed, 04 Nov 2009 22:51:27 +0100 |
ballarin |
Use PrintMode.setmp to make thread-safe; avoid code clones.
|
file |
diff |
annotate
|
| Mon, 02 Nov 2009 22:51:22 +0100 |
ballarin |
Make output indenpendent of current print mode.
|
file |
diff |
annotate
|
| Mon, 02 Nov 2009 21:27:26 +0100 |
ballarin |
Relax on type agreement with original context when applying term syntax.
|
file |
diff |
annotate
|
| Sat, 26 Sep 2009 21:03:57 +0200 |
ballarin |
Stricter test: raise error if registration generates duplicate theorem.
|
file |
diff |
annotate
|
| Sat, 28 Mar 2009 00:13:01 +0100 |
ballarin |
Merged.
|
file |
diff |
annotate
|
| Fri, 27 Mar 2009 20:25:07 +0100 |
ballarin |
Comments updated.
|
file |
diff |
annotate
|
| Thu, 26 Mar 2009 20:08:55 +0100 |
wenzelm |
interpretation/interpret: prefixes are mandatory by default;
|
file |
diff |
annotate
|
| Fri, 16 Jan 2009 15:14:16 +0100 |
haftmann |
adapted to changes in class package
|
file |
diff |
annotate
|
| Thu, 15 Jan 2009 14:52:23 +0100 |
haftmann |
decativate Toplevel.debug after reading
|
file |
diff |
annotate
|
| Mon, 05 Jan 2009 15:35:42 +0100 |
haftmann |
removed locale adaption layer
|
file |
diff |
annotate
| base
|
| Thu, 16 Oct 2008 17:19:47 +0200 |
ballarin |
More occurrences of 'includes' gone.
|
file |
diff |
annotate
|
| Tue, 16 Sep 2008 12:26:15 +0200 |
ballarin |
No interpretation of locale with dangling type frees.
|
file |
diff |
annotate
|
| Tue, 02 Sep 2008 17:31:20 +0200 |
ballarin |
Interpretation commands no longer accept interpretation attributes.
|
file |
diff |
annotate
|
| Wed, 06 Aug 2008 16:41:40 +0200 |
ballarin |
Interpretation command (theory/proof context) no longer simplifies goal.
|
file |
diff |
annotate
|
| Mon, 04 Aug 2008 10:37:33 +0200 |
ballarin |
Updated locale tests.
|
file |
diff |
annotate
|
| Fri, 25 Jul 2008 12:03:32 +0200 |
haftmann |
dropped locale (open)
|
file |
diff |
annotate
|
| Wed, 16 Jul 2008 14:21:57 +0200 |
ballarin |
Removed uses of context element includes.
|
file |
diff |
annotate
|
| Mon, 14 Apr 2008 17:54:56 +0200 |
ballarin |
Changed naming scheme for theorems generated by interpretations.
|
file |
diff |
annotate
|
| Thu, 20 Mar 2008 00:20:44 +0100 |
wenzelm |
simplified get_thm(s): back to plain name argument;
|
file |
diff |
annotate
|
| Wed, 19 Mar 2008 22:27:57 +0100 |
wenzelm |
renamed datatype thmref to Facts.ref, tuned interfaces;
|
file |
diff |
annotate
|
| Wed, 05 Mar 2008 21:24:03 +0100 |
wenzelm |
explicit referencing of background facts;
|
file |
diff |
annotate
|
| Mon, 05 Nov 2007 17:47:52 +0100 |
ballarin |
Tests enforce proper export behaviour.
|
file |
diff |
annotate
|
| Mon, 01 Oct 2007 12:24:45 +0200 |
ballarin |
unfold_locales workaround
|
file |
diff |
annotate
|
| Fri, 31 Aug 2007 18:46:33 +0200 |
wenzelm |
do not touch quick_and_dirty;
|
file |
diff |
annotate
|
| Mon, 23 Jul 2007 13:48:30 +0200 |
ballarin |
interpretation: equations are propositions not pairs of terms;
|
file |
diff |
annotate
|
| Fri, 11 May 2007 00:43:45 +0200 |
wenzelm |
tuned proofs;
|
file |
diff |
annotate
|
| Fri, 20 Apr 2007 16:55:38 +0200 |
ballarin |
Interpretation equations applied to attributes
|
file |
diff |
annotate
|
| Fri, 13 Apr 2007 10:02:30 +0200 |
ballarin |
Experimental code for the interpretation of definitions.
|
file |
diff |
annotate
|
| Mon, 04 Sep 2006 15:27:30 +0200 |
ballarin |
More locale test code.
|
file |
diff |
annotate
|
| Fri, 07 Jul 2006 09:24:05 +0200 |
ballarin |
Modified comment.
|
file |
diff |
annotate
|
| Tue, 04 Jul 2006 14:47:01 +0200 |
ballarin |
Method intro_locales replaced by intro_locales and unfold_locales.
|
file |
diff |
annotate
|
| Tue, 20 Jun 2006 15:53:44 +0200 |
ballarin |
Restructured locales with predicates: import is now an interpretation.
|
file |
diff |
annotate
|
| Tue, 06 Jun 2006 10:05:57 +0200 |
ballarin |
Improved parameter management of locales.
|
file |
diff |
annotate
|
| Fri, 16 Sep 2005 14:44:52 +0200 |
ballarin |
tuned
|
file |
diff |
annotate
|
| Fri, 02 Sep 2005 09:50:58 +0200 |
ballarin |
print_locale omits facts by default
|
file |
diff |
annotate
|
| Wed, 24 Aug 2005 12:07:00 +0200 |
ballarin |
Printing of interpretations: option to show witness theorems;
|
file |
diff |
annotate
|
| Wed, 17 Aug 2005 17:04:15 +0200 |
ballarin |
Improved generation of witnesses in interpretation.
|
file |
diff |
annotate
|
| Mon, 08 Aug 2005 22:11:31 +0200 |
ballarin |
Release of interpretation in locale.
|
file |
diff |
annotate
|
| Tue, 02 Aug 2005 16:52:21 +0200 |
ballarin |
First version of interpretation in locales. Not yet fully functional.
|
file |
diff |
annotate
|
| Thu, 07 Jul 2005 15:52:31 +0200 |
ballarin |
Preparations for interpretation of locales in locales.
|
file |
diff |
annotate
|
| Thu, 30 Jun 2005 14:06:29 +0200 |
ballarin |
Proper treatment of beta-redexes in witness theorems.
|
file |
diff |
annotate
|
| Wed, 08 Jun 2005 16:11:09 +0200 |
ballarin |
Fixed "axiom" generation for mixed locales with and without predicates.
|
file |
diff |
annotate
|
| Wed, 01 Jun 2005 12:30:49 +0200 |
ballarin |
Locales: new element constrains, parameter renaming with syntax,
|
file |
diff |
annotate
|
| Fri, 27 May 2005 16:24:48 +0200 |
ballarin |
Locale expressions: rename with optional mixfix syntax.
|
file |
diff |
annotate
|
| Mon, 25 Apr 2005 17:58:41 +0200 |
ballarin |
Subsumption of locale interpretations.
|
file |
diff |
annotate
|
| Mon, 18 Apr 2005 09:25:23 +0200 |
ballarin |
Interpretation supports statically scoped attributes; documentation.
|
file |
diff |
annotate
|
| Mon, 11 Apr 2005 12:34:34 +0200 |
ballarin |
First release of interpretation commands.
|
file |
diff |
annotate
|
| Thu, 24 Mar 2005 17:03:37 +0100 |
ballarin |
Further work on interpretation commands. New command `interpret' for
|
file |
diff |
annotate
|
| Thu, 10 Mar 2005 17:48:36 +0100 |
ballarin |
Registrations of global locale interpretations: improved, better naming.
|
file |
diff |
annotate
|
| Wed, 09 Mar 2005 18:44:52 +0100 |
ballarin |
First version of global registration command.
|
file |
diff |
annotate
|