Mon, 05 Sep 2022 21:18:40 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
Mon, 05 Sep 2022 21:13:29 +0200 |
wenzelm |
show goal instantiation, notably for 'schematic_goal' command (inactive by default);
|
file |
diff |
annotate
|
Wed, 20 Oct 2021 18:13:17 +0200 |
wenzelm |
discontinued obsolete "val extend = I" for data slots;
|
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
|
Wed, 18 Aug 2021 23:04:58 +0200 |
wenzelm |
support configuration options "show_results";
|
file |
diff |
annotate
|
Tue, 03 Aug 2021 13:08:23 +0200 |
wenzelm |
more uniform signatures in ML and Scala;
|
file |
diff |
annotate
|
Fri, 16 Aug 2019 10:33:25 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Mon, 03 Jun 2019 13:28:01 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Thu, 03 Jan 2019 14:12:44 +0100 |
wenzelm |
clarified signature: more types;
|
file |
diff |
annotate
|
Tue, 27 Nov 2018 21:07:39 +0100 |
wenzelm |
more accurate positions for "name" (quoted string) and "embedded" (cartouche): refer to content without delimiters, which is e.g. relevant for systematic selection/renaming of scope groups;
|
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
|
Mon, 27 Aug 2018 14:42:24 +0200 |
wenzelm |
support named ML environments, notably "Isabelle", "SML";
|
file |
diff |
annotate
|
Sun, 01 Jul 2018 12:38:37 +0200 |
wenzelm |
discontinued pending_shyps: too much complication due to lazy facts;
|
file |
diff |
annotate
|