| Sat, 04 Sep 2021 21:25:08 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Wed, 09 Jun 2021 18:04:21 +0000 |
haftmann |
more succint interfaces
|
file |
diff |
annotate
|
| Thu, 29 Oct 2020 18:23:28 +0000 |
haftmann |
unified Local_Theory.init with Generic_Target.init
|
file |
diff |
annotate
|
| Sat, 24 Oct 2020 15:16:54 +0000 |
haftmann |
tuned interfaces
|
file |
diff |
annotate
|
| Thu, 21 Feb 2019 09:15:07 +0000 |
haftmann |
streamlined specification interfaces
|
file |
diff |
annotate
|
| Wed, 06 Dec 2017 18:59:33 +0100 |
wenzelm |
prefer control symbol antiquotations;
|
file |
diff |
annotate
|
| Fri, 04 Aug 2017 08:12:58 +0200 |
haftmann |
more structural sharing between common target Generic_Target.init
|
file |
diff |
annotate
|
| Fri, 04 Aug 2017 08:12:54 +0200 |
haftmann |
treat exit separate from regular local theory operations
|
file |
diff |
annotate
|
| Sun, 18 Dec 2016 13:07:13 +0100 |
wenzelm |
tuned messages -- more symbols;
|
file |
diff |
annotate
|
| 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
|