# HG changeset patch # User wenzelm # Date 975611880 -3600 # Node ID dc615fccc1e6e606b595110e01cd01e13a0d8a6f # Parent e574274823a4eed5700bc4cfedba642e2b7ba937 tuned; diff -r e574274823a4 -r dc615fccc1e6 NEWS --- 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;