| Thu, 28 Oct 2021 12:09:58 +0200 |
wenzelm |
clarified keywords: major take precedence for commands, but not used for antiquotations;
|
file |
diff |
annotate
|
| Sun, 24 Oct 2021 16:43:54 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Thu, 21 Oct 2021 18:10:51 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Wed, 20 Oct 2021 20:25:33 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Wed, 20 Oct 2021 18:13:17 +0200 |
wenzelm |
discontinued obsolete "val extend = I" for data slots;
|
file |
diff |
annotate
|
| Wed, 20 Oct 2021 16:45:10 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Wed, 20 Oct 2021 16:36:49 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Tue, 07 Sep 2021 21:16:22 +0200 |
wenzelm |
export other entities, e.g. relevant for formal document output;
|
file |
diff |
annotate
|
| Mon, 06 Sep 2021 12:23:06 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Tue, 03 Aug 2021 13:08:23 +0200 |
wenzelm |
more uniform signatures in ML and Scala;
|
file |
diff |
annotate
|
| Wed, 27 May 2020 20:02:02 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 03 Apr 2020 17:35:10 +0200 |
wenzelm |
less redundant markup reports;
|
file |
diff |
annotate
|
| Tue, 13 Aug 2019 15:34:46 +0200 |
wenzelm |
added SUBPROOFS / "subproofs" method combinator, for more compact proofterms;
|
file |
diff |
annotate
|
| Tue, 13 Aug 2019 10:27:21 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Thu, 03 Jan 2019 14:12:44 +0100 |
wenzelm |
clarified signature: more types;
|
file |
diff |
annotate
|
| Wed, 31 Oct 2018 15:53:32 +0100 |
wenzelm |
clarified ML_Context.expression: it is a closed expression, not a let-declaration -- thus source positions are more accurate (amending d8849cfad60f, 162a4c2e97bc);
|
file |
diff |
annotate
|
| Thu, 25 Oct 2018 21:29:08 +0200 |
wenzelm |
clarified ML position: proper markup for def/ref scopes (see also 162a4c2e97bc);
|
file |
diff |
annotate
|
| Mon, 27 Aug 2018 20:43:01 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Thu, 25 Jan 2018 11:29:52 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Wed, 24 Jan 2018 20:47:36 +0100 |
wenzelm |
clarified operations;
|
file |
diff |
annotate
|
| Wed, 06 Dec 2017 18:59:33 +0100 |
wenzelm |
prefer control symbol antiquotations;
|
file |
diff |
annotate
|
| Tue, 13 Dec 2016 11:51:42 +0100 |
wenzelm |
more symbols;
|
file |
diff |
annotate
|
| Wed, 20 Jul 2016 11:44:11 +0200 |
wenzelm |
moved method "use" to Pure;
|
file |
diff |
annotate
|
| Wed, 08 Jun 2016 11:53:43 +0200 |
wenzelm |
provide dynamic facts in static context, to allow use of method_facts during static closure;
|
file |
diff |
annotate
|
| Wed, 08 Jun 2016 11:33:56 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 07 Jun 2016 19:57:41 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Tue, 07 Jun 2016 19:55:45 +0200 |
wenzelm |
clean facts more uniformly;
|
file |
diff |
annotate
|
| Tue, 07 Jun 2016 15:44:18 +0200 |
wenzelm |
expode method_facts via dynamic method context;
|
file |
diff |
annotate
|
| Thu, 12 May 2016 22:06:18 +0200 |
wenzelm |
common entity definitions within a global or local theory context;
|
file |
diff |
annotate
|
| Wed, 13 Apr 2016 18:01:05 +0200 |
wenzelm |
eliminated "xname" and variants;
|
file |
diff |
annotate
|