| Wed, 30 Mar 2016 19:31:28 +0200 |
wenzelm |
tuned messages -- position is usually missing here;
|
file |
diff |
annotate
|
| Tue, 29 Mar 2016 21:17:29 +0200 |
wenzelm |
more position information for type mixfix;
|
file |
diff |
annotate
|
| Sat, 19 Dec 2015 11:05:04 +0100 |
haftmann |
abandoned attempt to unify sublocale and interpretation into global theories
|
file |
diff |
annotate
|
| Mon, 01 Jun 2015 18:59:20 +0200 |
haftmann |
explicit argument expansion of uncheck rules;
|
file |
diff |
annotate
|
| Mon, 01 Jun 2015 18:59:20 +0200 |
haftmann |
clearly separated target primitives (target_foo) from self-contained target operations (foo)
|
file |
diff |
annotate
|
| Mon, 01 Jun 2015 18:59:20 +0200 |
haftmann |
dedicated config options to deactivate uncheck phase for improvable syntax
|
file |
diff |
annotate
|
| Mon, 01 Jun 2015 18:59:19 +0200 |
haftmann |
clarified interfaces for improvable syntax
|
file |
diff |
annotate
|
| Sun, 03 May 2015 18:13:15 +0200 |
wenzelm |
tuned output;
|
file |
diff |
annotate
|
| Tue, 31 Mar 2015 11:56:21 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 19 Dec 2014 12:36:50 +0100 |
wenzelm |
tuned;
|
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, 03 Feb 2014 16:33:54 +0100 |
wenzelm |
more formal markup;
|
file |
diff |
annotate
|
| Tue, 30 Jul 2013 15:09:25 +0200 |
wenzelm |
type theory is purely value-oriented;
|
file |
diff |
annotate
|
| Tue, 03 Apr 2012 13:47:15 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 03 Apr 2012 10:59:20 +0200 |
wenzelm |
more uniform theory_abbrev with const_declaration;
|
file |
diff |
annotate
|
| Mon, 02 Apr 2012 21:49:27 +0200 |
wenzelm |
clarified standard_declaration vs. theory_declaration;
|
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 14:29:22 +0200 |
wenzelm |
Local_Theory.map_contexts with explicit level indication: 0 = main target at bottom;
|
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 10:49:31 +0100 |
wenzelm |
synchronize syntax uniformly for target stack and aux. context;
|
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
|
| Wed, 14 Mar 2012 18:09:05 +0100 |
wenzelm |
tuned messages;
|
file |
diff |
annotate
|
| Wed, 14 Mar 2012 11:45:16 +0100 |
wenzelm |
Local_Theory.define no longer hard-wires default theorem name -- targets/packages need to take care of it;
|
file |
diff |
annotate
|
| Thu, 10 Nov 2011 17:47:25 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 09 Nov 2011 20:47:11 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 30 Oct 2011 22:20:45 +0100 |
wenzelm |
removed obsolete argument (cf. aa35859c8741);
|
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
|