| Mon, 13 Oct 2014 21:41:29 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 02 Jul 2014 08:03:50 +0200 |
haftmann |
optional exit hook for theory-like targets
|
file |
diff |
annotate
|
| Wed, 02 Jul 2014 08:03:49 +0200 |
haftmann |
restore exactly named target, prevent non-named targets to participate in the ad-hoc switch game
|
file |
diff |
annotate
|
| Wed, 02 Jul 2014 08:03:48 +0200 |
haftmann |
centralized (ad-hoc) switching of targets in named_target.ML
|
file |
diff |
annotate
|
| Sun, 08 Jun 2014 23:30:53 +0200 |
haftmann |
tuned data structure
|
file |
diff |
annotate
|
| Sun, 08 Jun 2014 23:30:52 +0200 |
haftmann |
recovered level-free fishing for locale, accidentally lost in dce365931721
|
file |
diff |
annotate
|
| Sun, 08 Jun 2014 23:30:51 +0200 |
haftmann |
self-contained locale_declaration operation
|
file |
diff |
annotate
|
| Sun, 08 Jun 2014 23:30:51 +0200 |
haftmann |
yet another attempt for terminology: foo_target_bar denotes an operation bar operating solely on the target context of target foo, foo_bar denotes a whole stack of operations to accomplish bar for target foo
|
file |
diff |
annotate
|
| Sat, 07 Jun 2014 08:16:03 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Sat, 07 Jun 2014 08:16:03 +0200 |
haftmann |
avoid odd Named_Target.reinit altogether
|
file |
diff |
annotate
|
| Sat, 07 Jun 2014 08:16:03 +0200 |
haftmann |
less baroque interface
|
file |
diff |
annotate
|
| Fri, 06 Jun 2014 19:19:46 +0200 |
haftmann |
dropped obscure and unused ad-hoc before_exit hook for named targets
|
file |
diff |
annotate
|
| Thu, 05 Jun 2014 19:39:38 +0200 |
haftmann |
sharpened criterion: bare named target is only at the bottom level
|
file |
diff |
annotate
|
| Thu, 05 Jun 2014 19:39:35 +0200 |
haftmann |
tuned
|
file |
diff |
annotate
|
| Mon, 02 Jun 2014 19:21:41 +0200 |
haftmann |
formal treatment of dangling parameters for class abbrevs analogously to class consts
|
file |
diff |
annotate
|
| Mon, 02 Jun 2014 19:21:40 +0200 |
haftmann |
explicit passing of params
|
file |
diff |
annotate
|
| Fri, 30 May 2014 08:23:07 +0200 |
haftmann |
tuned signature
|
file |
diff |
annotate
|
| Thu, 29 May 2014 22:46:21 +0200 |
haftmann |
more direct passing of right-hand side
|
file |
diff |
annotate
|
| Wed, 28 May 2014 19:17:32 +0200 |
haftmann |
tuned variable names
|
file |
diff |
annotate
|
| Thu, 22 May 2014 17:53:02 +0200 |
haftmann |
tuned names
|
file |
diff |
annotate
|
| Thu, 22 May 2014 17:53:01 +0200 |
haftmann |
tuned signature
|
file |
diff |
annotate
|
| Thu, 22 May 2014 17:53:01 +0200 |
haftmann |
moved const declaration further down in bootstrap hierarchy: keep Named_Target free of low-level stuff
|
file |
diff |
annotate
|
| Thu, 22 May 2014 17:52:59 +0200 |
haftmann |
unused
|
file |
diff |
annotate
|
| Thu, 22 May 2014 16:59:49 +0200 |
haftmann |
common background_abbrev operation
|
file |
diff |
annotate
|
| Thu, 22 May 2014 16:59:49 +0200 |
haftmann |
tuned signature
|
file |
diff |
annotate
|
| Thu, 22 May 2014 16:59:49 +0200 |
haftmann |
tuned: prefer separate function trails for locales and classes rather than ad-hoc case distinction
|
file |
diff |
annotate
|
| Thu, 22 May 2014 16:59:49 +0200 |
haftmann |
compactified
|
file |
diff |
annotate
|
| Thu, 22 May 2014 09:40:05 +0200 |
haftmann |
compactified level discriminator
|
file |
diff |
annotate
|
| 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
|