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
|