diff -r 092e77b6f7c6 -r 89934cd022a9 NEWS --- a/NEWS Fri Jul 31 10:52:08 1998 +0200 +++ b/NEWS Fri Jul 31 10:54:39 1998 +0200 @@ -141,9 +141,9 @@ ancestor. - The specific .induct_tac no longer exists - use the generic induct_tac instead. - - natE has been renamed to nat.exhaustion - use exhaust_tac + - natE has been renamed to nat.exhaust - use exhaust_tac instead of res_inst_tac ... natE. Note that the variable - names in nat.exhaustion differ from the names in natE, this + names in nat.exhaust differ from the names in natE, this may cause some "fragile" proofs to fail. - The theorems split__case and split__case_asm have been renamed to .split and .split_asm.