| Tue, 23 May 2023 18:46:15 +0200 |
wenzelm |
tuned signature: more position information;
|
file |
diff |
annotate
|
| Wed, 20 Oct 2021 18:13:17 +0200 |
wenzelm |
discontinued obsolete "val extend = I" for data slots;
|
file |
diff |
annotate
|
| Mon, 12 Oct 2020 07:25:38 +0000 |
haftmann |
consolidated names and operations
|
file |
diff |
annotate
|
| Fri, 14 Aug 2020 14:40:24 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Fri, 09 Aug 2019 17:14:49 +0200 |
wenzelm |
formal position for PThm nodes;
|
file |
diff |
annotate
|
| Fri, 04 Jan 2019 23:22:53 +0100 |
wenzelm |
isabelle update -u control_cartouches;
|
file |
diff |
annotate
|
| Fri, 23 Feb 2018 19:25:37 +0100 |
wenzelm |
added HOLogic.mk_obj_eq convenience and eliminated some clones;
|
file |
diff |
annotate
|
| Wed, 28 Dec 2016 17:22:16 +0100 |
blanchet |
print constants in 'primrec', 'primcorec(ursive)', 'corec(ursive)', like in 'definition' and 'fun(ction)'
|
file |
diff |
annotate
|
| Wed, 21 Dec 2016 12:49:15 +0100 |
blanchet |
generalized ML function (towards nonuniform datatypes)
|
file |
diff |
annotate
|
| Mon, 24 Oct 2016 20:32:02 +0200 |
blanchet |
more accurate error message
|
file |
diff |
annotate
|
| Mon, 12 Sep 2016 23:17:55 +0200 |
blanchet |
make (co)induct component of 'fp_sugar' optional, for the benefit of nonuniform (co)datatypes and other similar extensions
|
file |
diff |
annotate
|
| Sun, 11 Sep 2016 23:32:45 +0200 |
blanchet |
generalized code towards nonuniform (co)datatypes
|
file |
diff |
annotate
|
| Thu, 08 Sep 2016 10:16:37 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Tue, 06 Sep 2016 11:21:21 +0200 |
blanchet |
extended ML signature
|
file |
diff |
annotate
|
| Tue, 23 Aug 2016 15:19:32 +0200 |
traytel |
tuned signature
|
file |
diff |
annotate
|
| Sun, 14 Aug 2016 12:26:09 +0200 |
blanchet |
tuned message
|
file |
diff |
annotate
|
| Thu, 23 Jun 2016 11:01:14 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 21 Jun 2016 17:35:45 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 02 Jun 2016 16:49:44 +0200 |
wenzelm |
eliminated pointless alias (no warning for duplicates);
|
file |
diff |
annotate
|
| Tue, 31 May 2016 10:53:10 +0200 |
blanchet |
error message
|
file |
diff |
annotate
|
| Mon, 30 May 2016 14:15:44 +0200 |
wenzelm |
allow 'for' fixes for multi_specs;
|
file |
diff |
annotate
|
| Thu, 28 Apr 2016 09:43:11 +0200 |
wenzelm |
support 'assumes' in specifications, e.g. 'definition', 'inductive';
|
file |
diff |
annotate
|
| Thu, 07 Apr 2016 17:56:26 +0200 |
traytel |
(un)folds are not legacy
|
file |
diff |
annotate
|
| Tue, 05 Apr 2016 09:54:17 +0200 |
traytel |
single uniqueness theorems for map, (un)fold, (co)rec for mutual (co)datatypes
|
file |
diff |
annotate
|
| Tue, 29 Mar 2016 19:17:05 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Mon, 28 Mar 2016 12:05:47 +0200 |
blanchet |
avoid 'prove_sorry' for unreliable tactics
|
file |
diff |
annotate
|
| Mon, 28 Mar 2016 12:05:47 +0200 |
blanchet |
tuning
|
file |
diff |
annotate
|
| Mon, 28 Mar 2016 12:05:47 +0200 |
blanchet |
added '_legacy' suffixes
|
file |
diff |
annotate
|
| Wed, 23 Mar 2016 16:37:13 +0100 |
blanchet |
sorted out type issue with sort constraints
|
file |
diff |
annotate
|
| Tue, 22 Mar 2016 12:39:37 +0100 |
blanchet |
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
|
file |
diff |
annotate
|