| Mon, 02 Dec 2019 15:04:38 +0100 |
wenzelm |
proper spec_rule name via naming/binding/Morphism.binding;
|
file |
diff |
annotate
|
| Fri, 29 Nov 2019 20:57:04 +0100 |
wenzelm |
more informative spec rules: optional name;
|
file |
diff |
annotate
|
| Tue, 27 Aug 2019 13:22:33 +0200 |
wenzelm |
proper positions for 'termination' command (see also 5549e686d6ac);
|
file |
diff |
annotate
|
| Tue, 27 Aug 2019 11:02:08 +0200 |
wenzelm |
tuned names -- proper scopes;
|
file |
diff |
annotate
|
| Sun, 25 Aug 2019 22:17:24 +0200 |
wenzelm |
proper positions for 'termination' command instead of original 'function' command, e.g. relevant for isabelle mmt_import;
|
file |
diff |
annotate
|
| Fri, 09 Aug 2019 17:14:49 +0200 |
wenzelm |
formal position for PThm nodes;
|
file |
diff |
annotate
|
| Tue, 26 Mar 2019 22:13:36 +0100 |
wenzelm |
more informative Spec_Rules.Equational, notably primrec argument types;
|
file |
diff |
annotate
|
| Fri, 23 Feb 2018 20:55:46 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 16 Feb 2018 22:16:50 +0100 |
wenzelm |
tuned signature (again);
|
file |
diff |
annotate
|
| Fri, 16 Feb 2018 21:33:04 +0100 |
wenzelm |
trim context of persistent data;
|
file |
diff |
annotate
|
| Wed, 06 Dec 2017 20:43:09 +0100 |
wenzelm |
prefer control symbol antiquotations;
|
file |
diff |
annotate
|
| Sun, 02 Jul 2017 20:13:38 +0200 |
haftmann |
proper concept of code declaration wrt. atomicity and Isar declarations
|
file |
diff |
annotate
|
| Wed, 05 Apr 2017 10:26:28 +0200 |
Lars Hupel |
store totality fact in function info
|
file |
diff |
annotate
|
| Mon, 06 Jun 2016 21:28:46 +0200 |
haftmann |
explicit tagging of code equations de-baroquifies interface
|
file |
diff |
annotate
|
| Mon, 30 May 2016 20:58:16 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|