equal
deleted
inserted
replaced
58 the rest of the goal is passed through the induction; |
58 the rest of the goal is passed through the induction; |
59 - 'induct' proper support for mutual induction involving non-atomic |
59 - 'induct' proper support for mutual induction involving non-atomic |
60 rule statements (uses the new concept of simultaneous goals, see |
60 rule statements (uses the new concept of simultaneous goals, see |
61 below); |
61 below); |
62 - removed obsolete "(simplified)" and "(stripped)" options of methods; |
62 - removed obsolete "(simplified)" and "(stripped)" options of methods; |
63 - added 'print_induct_rules' (covered by help item in Proof General > 3.3); |
63 - undeclared rule case names default to numbers 1, 2, 3, ...; |
|
64 - added 'print_induct_rules' (covered by help item in recent Proof |
|
65 General versions); |
64 - moved induct/cases attributes to Pure, methods to Provers; |
66 - moved induct/cases attributes to Pure, methods to Provers; |
65 - generic method setup instantiated for FOL and HOL; |
67 - generic method setup instantiated for FOL and HOL; |
66 |
68 |
67 * Pure: support multiple simultaneous goal statements, for example |
69 * Pure: support multiple simultaneous goal statements, for example |
68 "have a: A and b: B" (same for 'theorem' etc.); being a pure |
70 "have a: A and b: B" (same for 'theorem' etc.); being a pure |