equal
deleted
inserted
replaced
82 * Pure: 'thm_deps' command visualizes dependencies of theorems and |
82 * Pure: 'thm_deps' command visualizes dependencies of theorems and |
83 lemmas, using the graph browser tool; |
83 lemmas, using the graph browser tool; |
84 |
84 |
85 * Pure: predict failure of "show" in interactive mode; |
85 * Pure: predict failure of "show" in interactive mode; |
86 |
86 |
|
87 * Pure: 'thms_containing' now takes actual terms as arguments; |
|
88 |
87 * HOL: improved method 'induct' --- now handles non-atomic goals |
89 * HOL: improved method 'induct' --- now handles non-atomic goals |
88 (potential INCOMPATIBILITY); tuned error handling; |
90 (potential INCOMPATIBILITY); tuned error handling; |
89 |
91 |
90 * HOL: cases and induct rules now provide explicit hints about the |
92 * HOL: cases and induct rules now provide explicit hints about the |
91 number of facts to be consumed (0 for "type" and 1 for "set" rules); |
93 number of facts to be consumed (0 for "type" and 1 for "set" rules); |
94 * HOL: local contexts (aka cases) may now contain term bindings as |
96 * HOL: local contexts (aka cases) may now contain term bindings as |
95 well; the 'cases' and 'induct' methods new provide a ?case binding for |
97 well; the 'cases' and 'induct' methods new provide a ?case binding for |
96 the result to be shown in each case; |
98 the result to be shown in each case; |
97 |
99 |
98 * HOL: added 'recdef_tc' command; |
100 * HOL: added 'recdef_tc' command; |
|
101 |
|
102 * isatool convert assists in eliminating legacy ML scripts; |
99 |
103 |
100 |
104 |
101 *** HOL *** |
105 *** HOL *** |
102 |
106 |
103 * HOL/Library: a collection of generic theories to be used together |
107 * HOL/Library: a collection of generic theories to be used together |