Tue, 16 Feb 2010 13:26:21 +0100 |
wenzelm |
comment;
|
file |
diff |
annotate
|
Sun, 07 Feb 2010 19:33:34 +0100 |
wenzelm |
renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
|
file |
diff |
annotate
|
Fri, 13 Nov 2009 21:11:15 +0100 |
wenzelm |
modernized structure Local_Theory;
|
file |
diff |
annotate
|
Fri, 13 Nov 2009 20:41:29 +0100 |
wenzelm |
eliminated slightly odd kind argument of LocalTheory.note(s);
|
file |
diff |
annotate
|
Thu, 12 Nov 2009 22:29:54 +0100 |
wenzelm |
eliminated slightly odd (unused) "axiom" and "assumption" -- collapsed to unspecific "";
|
file |
diff |
annotate
|
Thu, 12 Nov 2009 22:02:11 +0100 |
wenzelm |
eliminated obsolete "internal" kind -- collapsed to unspecific "";
|
file |
diff |
annotate
|
Tue, 10 Nov 2009 16:04:57 +0100 |
wenzelm |
modernized structure Theory_Target;
|
file |
diff |
annotate
|
Fri, 30 Oct 2009 13:59:52 +0100 |
haftmann |
tuned variable names of bindings; conceal predicate constants
|
file |
diff |
annotate
|
Thu, 29 Oct 2009 16:34:44 +0100 |
wenzelm |
eliminated obsolete/unused Thm.kind_internal/is_internal etc.;
|
file |
diff |
annotate
|
Wed, 28 Oct 2009 16:25:27 +0100 |
wenzelm |
conceal internal bindings;
|
file |
diff |
annotate
|
Sun, 25 Oct 2009 21:35:46 +0100 |
wenzelm |
eliminated obsolete tags for types/consts -- now handled via name space, in strongly typed fashion;
|
file |
diff |
annotate
|
Wed, 21 Oct 2009 10:15:31 +0200 |
haftmann |
removed old-style \ and \\ infixes
|
file |
diff |
annotate
|
Thu, 01 Oct 2009 20:52:18 +0200 |
ballarin |
Merged.
|
file |
diff |
annotate
|
Thu, 01 Oct 2009 20:37:33 +0200 |
ballarin |
Avoid administrative overhead for identity mixins.
|
file |
diff |
annotate
|
Thu, 01 Oct 2009 11:33:32 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
Thu, 01 Oct 2009 07:40:25 +0200 |
ballarin |
Merged.
|
file |
diff |
annotate
|
Tue, 29 Sep 2009 22:15:54 +0200 |
ballarin |
Propagation of mixins for interpretation; reactivated diagnostic command print_interps.
|
file |
diff |
annotate
|
Sat, 19 Sep 2009 18:43:11 +0200 |
ballarin |
Explicit management of registration mixins.
|
file |
diff |
annotate
|
Wed, 19 Aug 2009 19:35:46 +0200 |
ballarin |
Improved comments and api names.
|
file |
diff |
annotate
|
Wed, 30 Sep 2009 22:24:57 +0200 |
wenzelm |
eliminated redundant parameters;
|
file |
diff |
annotate
|
Thu, 03 Sep 2009 15:39:02 +0200 |
haftmann |
proper class syntax for sublocale class < expr
|
file |
diff |
annotate
|
Wed, 15 Jul 2009 18:20:08 +0200 |
haftmann |
simplification of locale interfaces
|
file |
diff |
annotate
|
Fri, 10 Jul 2009 07:59:44 +0200 |
haftmann |
merged
|
file |
diff |
annotate
|
Fri, 10 Jul 2009 07:59:29 +0200 |
haftmann |
tuned locale interface
|
file |
diff |
annotate
|
Thu, 09 Jul 2009 22:48:12 +0200 |
wenzelm |
renamed structure TermSubst to Term_Subst;
|
file |
diff |
annotate
|
Mon, 30 Mar 2009 15:16:58 +0200 |
wenzelm |
prep_full_context_statement: explicit record of flags;
|
file |
diff |
annotate
|
Sun, 29 Mar 2009 19:48:35 +0200 |
wenzelm |
merged
|
file |
diff |
annotate
|
Sun, 29 Mar 2009 17:38:01 +0200 |
ballarin |
Merged.
|
file |
diff |
annotate
|
Sun, 29 Mar 2009 17:22:17 +0200 |
ballarin |
Normalise equation only for morphism, not thm stored in theory.
|
file |
diff |
annotate
|
Sun, 29 Mar 2009 19:41:04 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|