Tue, 03 Apr 2012 09:41:16 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Mon, 02 Apr 2012 23:55:25 +0200 |
wenzelm |
more general standard_declaration;
|
file |
diff |
annotate
|
Mon, 02 Apr 2012 21:49:27 +0200 |
wenzelm |
clarified standard_declaration vs. theory_declaration;
|
file |
diff |
annotate
|
Mon, 02 Apr 2012 20:50:41 +0200 |
wenzelm |
smarter generic_const: plain alias for non-dependent case (e.g. prospective datatype or record syntax);
|
file |
diff |
annotate
|
Mon, 02 Apr 2012 20:12:17 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Mon, 02 Apr 2012 19:47:21 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Mon, 02 Apr 2012 19:10:52 +0200 |
wenzelm |
misc tuning and simplification;
|
file |
diff |
annotate
|
Sun, 01 Apr 2012 20:42:19 +0200 |
wenzelm |
nothing specific about named target;
|
file |
diff |
annotate
|
Sun, 01 Apr 2012 20:36:33 +0200 |
wenzelm |
clarified Generic_Target.notes: always perform Attrib.partial_evaluation;
|
file |
diff |
annotate
|
Sun, 01 Apr 2012 18:01:19 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Sun, 01 Apr 2012 15:23:43 +0200 |
wenzelm |
clarified Named_Target.target_declaration: propagate through other levels as well;
|
file |
diff |
annotate
|
Thu, 22 Mar 2012 15:41:49 +0100 |
wenzelm |
uniform Generic_Target.standard_declaration, which uses the standard morphism for each context (NB: targets like "interpretation" appear like "theory" but declare local type parameters);
|
file |
diff |
annotate
|
Thu, 22 Mar 2012 11:11:51 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Wed, 21 Mar 2012 23:26:35 +0100 |
wenzelm |
more explicit Toplevel.open_target/close_target;
|
file |
diff |
annotate
|
Wed, 21 Mar 2012 17:25:35 +0100 |
wenzelm |
basic support for nested contexts including bundles;
|
file |
diff |
annotate
|
Wed, 21 Mar 2012 11:25:19 +0100 |
wenzelm |
clarified Local_Theory.init: avoid hardwired naming policy, discontinued odd/unused group argument (cf. 5ee13e0428d2);
|
file |
diff |
annotate
|
Sat, 17 Mar 2012 23:50:47 +0100 |
wenzelm |
amended locale_declaration: avoid duplication of Local_Theory.target with global_morphism (cf. 57def0b39696) -- Haftmann-Wenzel Sandwich has 3 layers, not 4;
|
file |
diff |
annotate
|
Sun, 20 Nov 2011 17:57:09 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Fri, 18 Nov 2011 21:55:24 +0100 |
wenzelm |
partial evaluation of locale facts leads to static scoping of rule attributes;
|
file |
diff |
annotate
|
Mon, 14 Nov 2011 16:52:19 +0100 |
wenzelm |
pass positions for named targets, for formal links in the document model;
|
file |
diff |
annotate
|
Mon, 07 Nov 2011 17:00:23 +0100 |
wenzelm |
tuned signature -- avoid spurious Thm.mixed_attribute;
|
file |
diff |
annotate
|
Sun, 06 Nov 2011 21:51:46 +0100 |
wenzelm |
more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
|
file |
diff |
annotate
|
Sat, 05 Nov 2011 22:41:25 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Sat, 05 Nov 2011 22:01:19 +0100 |
wenzelm |
misc tuning;
|
file |
diff |
annotate
|
Sun, 30 Oct 2011 22:35:18 +0100 |
wenzelm |
even more uniform Local_Theory.declaration for locales (cf. 57def0b39696, aa35859c8741);
|
file |
diff |
annotate
|
Sun, 30 Oct 2011 22:20:45 +0100 |
wenzelm |
removed obsolete argument (cf. aa35859c8741);
|
file |
diff |
annotate
|
Sat, 29 Oct 2011 12:57:43 +0200 |
wenzelm |
uniform treatment of syntax declaration wrt. aux. context (NB: notation avoids duplicate mixfix internally);
|
file |
diff |
annotate
|
Fri, 28 Oct 2011 23:16:50 +0200 |
wenzelm |
refined Local_Theory.declaration {syntax = false, pervasive} semantics: update is applied to auxiliary context as well;
|
file |
diff |
annotate
|
Fri, 28 Oct 2011 22:17:30 +0200 |
wenzelm |
uniform Local_Theory.declaration with explicit params;
|
file |
diff |
annotate
|
Fri, 28 Oct 2011 17:15:52 +0200 |
wenzelm |
tuned signature -- refined terminology;
|
file |
diff |
annotate
|