| Fri, 25 Apr 2014 21:45:04 +0200 |
haftmann |
subscription as target-specific implementation device
|
file |
diff |
annotate
|
| Tue, 11 Mar 2014 22:49:28 +0100 |
wenzelm |
more efficient local theory operations, by imposing a linear change discipline on the main types/consts tables, in order to speed-up Proof_Context.transfer_syntax required for Local_Theory.raw_theory_result;
|
file |
diff |
annotate
|
| Wed, 26 Feb 2014 10:53:19 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 19 Aug 2013 20:47:09 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 25 May 2013 15:44:08 +0200 |
haftmann |
tuned structure
|
file |
diff |
annotate
|
| Tue, 21 May 2013 17:45:53 +0200 |
wenzelm |
more markup;
|
file |
diff |
annotate
|
| Mon, 18 Jun 2012 15:48:43 +0200 |
haftmann |
class target handles additional non-class term parameters appropriately
|
file |
diff |
annotate
|
| Tue, 03 Apr 2012 13:47:15 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 03 Apr 2012 11:28:21 +0200 |
wenzelm |
clarified generic_const vs. close_schematic_term;
|
file |
diff |
annotate
|
| Tue, 03 Apr 2012 10:59:20 +0200 |
wenzelm |
more uniform theory_abbrev with const_declaration;
|
file |
diff |
annotate
|
| Tue, 03 Apr 2012 09:47:20 +0200 |
wenzelm |
clarified background_foundation vs. theory_foundation (with const_declaration);
|
file |
diff |
annotate
|
| 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
|
| Sat, 16 Apr 2011 15:47:52 +0200 |
wenzelm |
modernized structure Proof_Context;
|
file |
diff |
annotate
|
| Sun, 13 Mar 2011 22:55:50 +0100 |
wenzelm |
tuned headers;
|
file |
diff |
annotate
|
| Sun, 16 Jan 2011 14:57:14 +0100 |
wenzelm |
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 |
wenzelm |
superficial tuning;
|
file |
diff |
annotate
|
| Wed, 22 Sep 2010 12:22:47 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Mon, 20 Sep 2010 16:05:25 +0200 |
wenzelm |
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 |
wenzelm |
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 |
haftmann |
tuned: less formal noise in Named_Target, more coherence in Class
|
file |
diff |
annotate
|
| Thu, 12 Aug 2010 13:53:42 +0200 |
haftmann |
Class.declare -> Class.const
|
file |
diff |
annotate
|
| Thu, 12 Aug 2010 13:42:13 +0200 |
haftmann |
named target is optional; explicit Name_Target.reinit
|
file |
diff |
annotate
|
| Thu, 12 Aug 2010 13:28:18 +0200 |
haftmann |
Named_Target.init: empty string represents theory target
|
file |
diff |
annotate
|
| Thu, 12 Aug 2010 13:23:46 +0200 |
haftmann |
Named_Target.theory_init
|
file |
diff |
annotate
|
| Wed, 11 Aug 2010 17:19:27 +0200 |
haftmann |
remove reinit operation alltogether
|
file |
diff |
annotate
|
| Wed, 11 Aug 2010 16:02:03 +0200 |
haftmann |
more convenient split of class modules: class and class_declaration
|
file |
diff |
annotate
|
| Wed, 11 Aug 2010 15:45:15 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Wed, 11 Aug 2010 14:45:38 +0200 |
haftmann |
renamed Theory_Target to the more appropriate Named_Target
|
file |
diff |
annotate
| base
|