equal
deleted
inserted
replaced
53 statements as well; |
53 statements as well; |
54 |
54 |
55 * HOL: improved method 'induct' --- now handles non-atomic goals |
55 * HOL: improved method 'induct' --- now handles non-atomic goals |
56 (potential INCOMPATIBILITY); tuned error handling; |
56 (potential INCOMPATIBILITY); tuned error handling; |
57 |
57 |
58 * HOL: cases and induct rules may now provide explicit hint about the |
58 * HOL: cases and induct rules now provide explicit hints about the |
59 number of facts to be consumed (0 for "type" and 1 for "set" rules); |
59 number of facts to be consumed (0 for "type" and 1 for "set" rules); |
60 any remaining facts are inserted into the goal verbatim; |
60 any remaining facts are inserted into the goal verbatim; |
61 |
61 |
62 |
62 |
63 *** HOL *** |
63 *** HOL *** |