Replaced nat.exhaustion by nat.exhaust
authorberghofe
Fri, 31 Jul 1998 10:54:39 +0200
changeset 5226 89934cd022a9
parent 5225 092e77b6f7c6
child 5227 e5a6ace920a0
Replaced nat.exhaustion by nat.exhaust
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 <typename>.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_<typename>_case and split_<typename>_case_asm
     have been renamed to <typename>.split and <typename>.split_asm.