equal
deleted
inserted
replaced
25 - added 'print_induct_rules' (covered by help item in Proof General > 3.3); |
25 - added 'print_induct_rules' (covered by help item in Proof General > 3.3); |
26 - generic setup instantiated for FOL and HOL; |
26 - generic setup instantiated for FOL and HOL; |
27 - removed obsolete "(simplified)" and "(stripped)" options; |
27 - removed obsolete "(simplified)" and "(stripped)" options; |
28 |
28 |
29 * Pure: renamed "antecedent" case to "rule_context"; |
29 * Pure: renamed "antecedent" case to "rule_context"; |
|
30 |
|
31 * Pure: added 'corollary' command; |
30 |
32 |
31 * Pure: fixed 'token_translation' command; |
33 * Pure: fixed 'token_translation' command; |
32 |
34 |
33 * HOL: 'recdef' now fails on unfinished automated proofs, use |
35 * HOL: 'recdef' now fails on unfinished automated proofs, use |
34 "(permissive)" option to recover old behavior; |
36 "(permissive)" option to recover old behavior; |