| #
14c7fb8f |
|
09-Aug-2019 |
wenzelm <none@none> |
formal position for PThm nodes;
|
| #
ed7a971e |
|
05-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
| #
a4bab154 |
|
04-Jan-2019 |
wenzelm <none@none> |
isabelle update -u control_cartouches;
|
| #
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
|
| #
a0ac0e86 |
|
06-Sep-2016 |
blanchet <none@none> |
extended ML signature + refactored
|
| #
6be02e3b |
|
29-Jul-2016 |
traytel <none@none> |
made generation of transfer goals more robust w.r.t. dead variables
|
| #
3dba35c1 |
|
27-May-2016 |
wenzelm <none@none> |
tuned proofs, to allow unfold_abs_def;
|
| #
b22e4c0f |
|
07-Oct-2015 |
blanchet <none@none> |
disable generation of 'case_transfer' for 'nibble', due to quadratic proof -- to make 'HOL-Proofs' happier
|
| #
e5517855 |
|
05-Oct-2015 |
traytel <none@none> |
collect the names from goals in favor of fragile exports
|
| #
839d9ae3 |
|
26-Jul-2015 |
wenzelm <none@none> |
updated to infer_instantiate;
|
| #
740a17d4 |
|
06-Mar-2015 |
wenzelm <none@none> |
Thm.cterm_of and Thm.ctyp_of operate on local context;
|
| #
b7bf58e6 |
|
03-Mar-2015 |
traytel <none@none> |
eliminated some clones of Proof_Context.cterm_of
|
| #
b4c4780a |
|
06-Jan-2015 |
blanchet <none@none> |
tuning
|
| #
1de6462a |
|
05-Jan-2015 |
blanchet <none@none> |
added plugins syntax to prim(co)rec
|
| #
ef71534e |
|
04-Jan-2015 |
blanchet <none@none> |
tuning
|
| #
07a7056b |
|
19-Dec-2014 |
desharna <none@none> |
Add plugin to generate transfer theorem for primrec and primcorec
|