changeset 10557 | dc615fccc1e6 |
parent 10547 | efaba354b7f1 |
child 10609 | 5cbb6e62c502 |
--- a/NEWS Thu Nov 30 20:14:25 2000 +0100 +++ b/NEWS Thu Nov 30 20:18:00 2000 +0100 @@ -55,7 +55,7 @@ * HOL: improved method 'induct' --- now handles non-atomic goals (potential INCOMPATIBILITY); tuned error handling; -* HOL: cases and induct rules may now provide explicit hint about the +* HOL: cases and induct rules now provide explicit hints about the number of facts to be consumed (0 for "type" and 1 for "set" rules); any remaining facts are inserted into the goal verbatim;