equal
deleted
inserted
replaced
59 (potential INCOMPATIBILITY); tuned error handling; |
59 (potential INCOMPATIBILITY); tuned error handling; |
60 |
60 |
61 * HOL: cases and induct rules now provide explicit hints about the |
61 * HOL: cases and induct rules now provide explicit hints about the |
62 number of facts to be consumed (0 for "type" and 1 for "set" rules); |
62 number of facts to be consumed (0 for "type" and 1 for "set" rules); |
63 any remaining facts are inserted into the goal verbatim; |
63 any remaining facts are inserted into the goal verbatim; |
|
64 |
|
65 * HOL: added 'recdef_tc' command; |
64 |
66 |
65 |
67 |
66 *** HOL *** |
68 *** HOL *** |
67 |
69 |
68 * HOL/Library: a collection of generic theories to be used together |
70 * HOL/Library: a collection of generic theories to be used together |