equal
deleted
inserted
replaced
21 * Isar/HOL: 'recdef' now fails on unfinished automated proofs, use |
21 * Isar/HOL: 'recdef' now fails on unfinished automated proofs, use |
22 "(permissive)" option to recover old behavior; |
22 "(permissive)" option to recover old behavior; |
23 |
23 |
24 * Isar/HOL: 'inductive' now longer features separate (collective) |
24 * Isar/HOL: 'inductive' now longer features separate (collective) |
25 attributes for 'intros'; |
25 attributes for 'intros'; |
|
26 |
|
27 * moved induct/cases attributes to Pure, added 'print_induct_rules' |
|
28 command; |
26 |
29 |
27 |
30 |
28 *** HOL *** |
31 *** HOL *** |
29 |
32 |
30 * HOL: linorder_less_split superseded by linorder_cases; |
33 * HOL: linorder_less_split superseded by linorder_cases; |