| Wed, 09 Jun 2021 18:04:21 +0000 |
haftmann |
more succint interfaces
|
file |
diff |
annotate
|
| Sat, 19 Dec 2020 09:33:11 +0000 |
haftmann |
clarified scope of concept
|
file |
diff |
annotate
|
| Fri, 18 Dec 2020 10:37:26 +0000 |
haftmann |
clarified name
|
file |
diff |
annotate
|
| Sun, 15 Nov 2020 07:17:05 +0000 |
haftmann |
type alias for mixin bundles
|
file |
diff |
annotate
|
| Sun, 01 Nov 2020 16:54:49 +0100 |
haftmann |
bundle mixins for locale and class specifications
|
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
|
| Mon, 12 Oct 2020 07:25:38 +0000 |
haftmann |
dedicated module for toplevel target handling
|
file |
diff |
annotate
|
| Wed, 23 Jan 2019 17:54:50 +0000 |
haftmann |
combinator to lift local theory update to theory update
|
file |
diff |
annotate
|
| Mon, 24 Sep 2018 19:34:14 +0200 |
wenzelm |
tuned signature: prefer value-oriented pretty-printing;
|
file |
diff |
annotate
|
| Thu, 15 Feb 2018 14:36:46 +0100 |
wenzelm |
recovered outer Pretty.block from 30c1639a343a, avoid excessive line breaks due to implicit Pretty.chunks;
|
file |
diff |
annotate
|
| Fri, 04 Aug 2017 08:13:00 +0200 |
haftmann |
tuned
|
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
|
| Fri, 04 Aug 2017 08:12:37 +0200 |
haftmann |
provide explicit variant initializers for regular named target vs. almost-named target
|
file |
diff |
annotate
|
| Fri, 04 Aug 2017 08:12:37 +0200 |
haftmann |
prefer explicit datatype over implicit sum;
|
file |
diff |
annotate
|
| Sat, 08 Jul 2017 20:05:26 +0200 |
haftmann |
clarified
|
file |
diff |
annotate
|
| Wed, 06 Jul 2016 11:29:51 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Thu, 23 Jun 2016 11:01:14 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Thu, 09 Jun 2016 12:16:52 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 05 Mar 2016 12:49:47 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 24 Jan 2016 14:58:56 +0100 |
wenzelm |
tuned;
|
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
|
| Thu, 03 Dec 2015 08:10:56 +0100 |
haftmann |
tuned sections
|
file |
diff |
annotate
|
| Mon, 01 Jun 2015 18:59:20 +0200 |
haftmann |
self-contained formulation of abbrev for named targets
|
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
|
| Sun, 03 May 2015 17:41:54 +0200 |
wenzelm |
tuned output;
|
file |
diff |
annotate
|
| Tue, 31 Mar 2015 17:34:52 +0200 |
wenzelm |
clarified role of naming for background theory: transform_binding (e.g. for "concealed" flag) uses naming of hypothetical context;
|
file |
diff |
annotate
|
| Tue, 31 Mar 2015 11:56:21 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 13 Oct 2014 21:41:29 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|