| Sat, 17 Mar 2012 23:50:47 +0100 |
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 |
tuned signature;
|
file | diff | annotate |
| Fri, 18 Nov 2011 21:55:24 +0100 |
partial evaluation of locale facts leads to static scoping of rule attributes;
|
file | diff | annotate |
| Mon, 14 Nov 2011 16:52:19 +0100 |
pass positions for named targets, for formal links in the document model;
|
file | diff | annotate |
| Mon, 07 Nov 2011 17:00:23 +0100 |
tuned signature -- avoid spurious Thm.mixed_attribute;
|
file | diff | annotate |
| Sun, 06 Nov 2011 21:51:46 +0100 |
more explicit representation of rule_attribute vs. declaration_attribute vs. mixed_attribute;
|
file | diff | annotate |
| Sat, 05 Nov 2011 22:41:25 +0100 |
tuned;
|
file | diff | annotate |
| Sat, 05 Nov 2011 22:01:19 +0100 |
misc tuning;
|
file | diff | annotate |
| Sun, 30 Oct 2011 22:35:18 +0100 |
even more uniform Local_Theory.declaration for locales (cf. 57def0b39696, aa35859c8741);
|
file | diff | annotate |
| Sun, 30 Oct 2011 22:20:45 +0100 |
removed obsolete argument (cf. aa35859c8741);
|
file | diff | annotate |
| Sat, 29 Oct 2011 12:57:43 +0200 |
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 |
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 |
uniform Local_Theory.declaration with explicit params;
|
file | diff | annotate |
| Fri, 28 Oct 2011 17:15:52 +0200 |
tuned signature -- refined terminology;
|
file | diff | annotate |
| Sat, 16 Apr 2011 15:47:52 +0200 |
modernized structure Proof_Context;
|
file | diff | annotate |
| Sun, 13 Mar 2011 22:55:50 +0100 |
tuned headers;
|
file | diff | annotate |
| Sun, 16 Jan 2011 14:57:14 +0100 |
added before_exit continuation for named targets (locale, class etc.), e.g. for final check/cleanup as in VC management;
|
file | diff | annotate |
| Sun, 28 Nov 2010 15:28:48 +0100 |
superficial tuning;
|
file | diff | annotate |
| Wed, 22 Sep 2010 12:22:47 +0200 |
tuned
|
file | diff | annotate |
| Mon, 20 Sep 2010 16:05:25 +0200 |
renamed structure PureThy to Pure_Thy and moved most content to Global_Theory, to emphasize that this is global-only;
|
file | diff | annotate |
| Thu, 26 Aug 2010 15:48:08 +0200 |
renamed Local_Theory.theory(_result) to Local_Theory.background_theory(_result) to emphasize that this belongs to the infrastructure and is rarely appropriate in user-space tools;
|
file | diff | annotate |
| Fri, 20 Aug 2010 08:52:01 +0200 |
tuned: less formal noise in Named_Target, more coherence in Class
|
file | diff | annotate |
| Thu, 12 Aug 2010 13:53:42 +0200 |
Class.declare -> Class.const
|
file | diff | annotate |
| Thu, 12 Aug 2010 13:42:13 +0200 |
named target is optional; explicit Name_Target.reinit
|
file | diff | annotate |
| Thu, 12 Aug 2010 13:28:18 +0200 |
Named_Target.init: empty string represents theory target
|
file | diff | annotate |
| Thu, 12 Aug 2010 13:23:46 +0200 |
Named_Target.theory_init
|
file | diff | annotate |
| Wed, 11 Aug 2010 17:19:27 +0200 |
remove reinit operation alltogether
|
file | diff | annotate |
| Wed, 11 Aug 2010 16:02:03 +0200 |
more convenient split of class modules: class and class_declaration
|
file | diff | annotate |
| Wed, 11 Aug 2010 15:45:15 +0200 |
tuned
|
file | diff | annotate |
| Wed, 11 Aug 2010 14:45:38 +0200 |
renamed Theory_Target to the more appropriate Named_Target
|
file | diff | annotate | base |