| Wed, 03 Sep 2008 17:47:40 +0200 |
wenzelm |
discontinued local axioms -- too difficult to implement, too easy to produce nonsense;
|
file |
diff |
annotate
|
| Tue, 02 Sep 2008 16:55:33 +0200 |
wenzelm |
type Attrib.binding abbreviates Name.binding without attributes;
|
file |
diff |
annotate
|
| Tue, 02 Sep 2008 14:10:45 +0200 |
wenzelm |
explicit type Name.binding for higher-specification elements;
|
file |
diff |
annotate
|
| Wed, 27 Aug 2008 11:48:54 +0200 |
wenzelm |
type Properties.T;
|
file |
diff |
annotate
|
| Mon, 25 Feb 2008 16:31:19 +0100 |
wenzelm |
maintain group in lthy data, implicit use in operations;
|
file |
diff |
annotate
|
| Sat, 26 Jan 2008 17:08:43 +0100 |
wenzelm |
grouped versions of axioms/define/notes;
|
file |
diff |
annotate
|
| Sat, 10 Nov 2007 18:36:10 +0100 |
wenzelm |
removed LocalTheory.target_naming/name;
|
file |
diff |
annotate
|
| Mon, 05 Nov 2007 20:50:42 +0100 |
wenzelm |
simplified LocalTheory.reinit;
|
file |
diff |
annotate
|
| Sat, 20 Oct 2007 18:54:33 +0200 |
wenzelm |
tuned abbrev interface;
|
file |
diff |
annotate
|
| Fri, 19 Oct 2007 20:57:14 +0200 |
wenzelm |
tuned interfaces;
|
file |
diff |
annotate
|
| Sun, 14 Oct 2007 00:18:07 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 13 Oct 2007 17:16:44 +0200 |
wenzelm |
renamed def to define;
|
file |
diff |
annotate
|
| Thu, 11 Oct 2007 21:10:40 +0200 |
wenzelm |
local_theory: incorporated consts into axioms;
|
file |
diff |
annotate
|
| Wed, 10 Oct 2007 17:31:56 +0200 |
wenzelm |
generalized notation interface (add or del);
|
file |
diff |
annotate
|
| Tue, 09 Oct 2007 17:10:46 +0200 |
wenzelm |
removed LocalTheory.defs/target_morphism operations;
|
file |
diff |
annotate
|
| Fri, 07 Sep 2007 20:40:08 +0200 |
wenzelm |
fixed type alias in signature;
|
file |
diff |
annotate
|
| Sat, 28 Jul 2007 22:01:06 +0200 |
wenzelm |
type Morphism.declaration;
|
file |
diff |
annotate
|
| Sat, 28 Jul 2007 20:40:24 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 07 May 2007 00:49:59 +0200 |
wenzelm |
simplified DataFun interfaces;
|
file |
diff |
annotate
|
| Sun, 04 Feb 2007 22:02:20 +0100 |
wenzelm |
added full_naming;
|
file |
diff |
annotate
|
| Sun, 28 Jan 2007 23:29:17 +0100 |
wenzelm |
added interface for target_naming;
|
file |
diff |
annotate
|
| Fri, 15 Dec 2006 00:08:15 +0100 |
wenzelm |
renamed LocalTheory.assert to affirm;
|
file |
diff |
annotate
|
| Tue, 12 Dec 2006 20:49:29 +0100 |
wenzelm |
abbrev: tuned signature;
|
file |
diff |
annotate
|
| Sun, 10 Dec 2006 15:30:42 +0100 |
wenzelm |
added notation/abbrev (from term_syntax.ML);
|
file |
diff |
annotate
|
| Thu, 07 Dec 2006 17:58:50 +0100 |
wenzelm |
moved notation/abbrevs to TermSyntax;
|
file |
diff |
annotate
|
| Wed, 06 Dec 2006 21:19:02 +0100 |
wenzelm |
abbrevs: actually observe target_morphism;
|
file |
diff |
annotate
|
| Tue, 05 Dec 2006 22:14:49 +0100 |
wenzelm |
notation/abbreviation: more serious handling of morphisms;
|
file |
diff |
annotate
|
| Thu, 30 Nov 2006 17:42:21 +0100 |
wenzelm |
added full_name;
|
file |
diff |
annotate
|
| Sun, 26 Nov 2006 18:07:24 +0100 |
wenzelm |
abbrevs: no result;
|
file |
diff |
annotate
|
| Thu, 23 Nov 2006 20:33:37 +0100 |
wenzelm |
uniform interface for type_syntax/term_syntax/declaration, dependent on morphism;
|
file |
diff |
annotate
|