| #
14c7fb8f |
|
09-Aug-2019 |
wenzelm <none@none> |
formal position for PThm nodes;
|
| #
a4bab154 |
|
04-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
| #
fcc9e542 |
|
23-Feb-2018 |
wenzelm <none@none> |
added HOLogic.mk_obj_eq convenience and eliminated some clones;
|
| #
bb1d3a61 |
|
28-Dec-2016 |
blanchet <none@none> |
print constants in 'primrec', 'primcorec(ursive)', 'corec(ursive)', like in 'definition' and 'fun(ction)'
|
| #
659a2dbd |
|
20-Dec-2016 |
blanchet <none@none> |
generalized ML function (towards nonuniform datatypes)
|
| #
f47963fb |
|
24-Oct-2016 |
blanchet <none@none> |
more accurate error message
|
| #
d945085c |
|
12-Sep-2016 |
blanchet <none@none> |
make (co)induct component of 'fp_sugar' optional, for the benefit of nonuniform (co)datatypes and other similar extensions
|
| #
63fa20eb |
|
11-Sep-2016 |
blanchet <none@none> |
generalized code towards nonuniform (co)datatypes
|
| #
79f97a31 |
|
08-Sep-2016 |
blanchet <none@none> |
tuning
|
| #
fa710cb8 |
|
06-Sep-2016 |
blanchet <none@none> |
extended ML signature
|
| #
41f01a69 |
|
23-Aug-2016 |
traytel <none@none> |
tuned signature
|
| #
da4c979b |
|
13-Aug-2016 |
blanchet <none@none> |
tuned message
|
| #
bee57ad5 |
|
23-Jun-2016 |
wenzelm <none@none> |
tuned signature;
|
| #
c71812c7 |
|
21-Jun-2016 |
wenzelm <none@none> |
tuned;
|
| #
237f0cff |
|
02-Jun-2016 |
wenzelm <none@none> |
eliminated pointless alias (no warning for duplicates);
|
| #
adca6a6b |
|
31-May-2016 |
blanchet <none@none> |
error message
|
| #
86d79029 |
|
30-May-2016 |
wenzelm <none@none> |
allow 'for' fixes for multi_specs;
|
| #
68f9ecca |
|
28-Apr-2016 |
wenzelm <none@none> |
support 'assumes' in specifications, e.g. 'definition', 'inductive';
tuned signatures;
|
| #
049cf95c |
|
07-Apr-2016 |
traytel <none@none> |
(un)folds are not legacy
|
| #
1a96a7b9 |
|
05-Apr-2016 |
traytel <none@none> |
single uniqueness theorems for map, (un)fold, (co)rec for mutual (co)datatypes
|
| #
c79d1ebb |
|
29-Mar-2016 |
blanchet <none@none> |
tuning
|
| #
b67fa4b8 |
|
27-Mar-2016 |
blanchet <none@none> |
avoid 'prove_sorry' for unreliable tactics
|
| #
dffe416d |
|
27-Mar-2016 |
blanchet <none@none> |
tuning
|
| #
4dd3178f |
|
27-Mar-2016 |
blanchet <none@none> |
added '_legacy' suffixes
|
| #
eb50c0fa |
|
23-Mar-2016 |
blanchet <none@none> |
sorted out type issue with sort constraints
|
| #
d80c5394 |
|
21-Mar-2016 |
blanchet <none@none> |
moved 'corec' from ssh://hg@bitbucket.org/jasmin_blanchette/nonprim-corec to Isabelle
|