Replaced nat.exhaustion by nat.exhaust
authorberghofe
Fri Jul 31 10:54:39 1998 +0200 (1998-07-31)
changeset 522689934cd022a9
parent 5225 092e77b6f7c6
child 5227 e5a6ace920a0
Replaced nat.exhaustion by nat.exhaust
NEWS
     1.1 --- a/NEWS	Fri Jul 31 10:52:08 1998 +0200
     1.2 +++ b/NEWS	Fri Jul 31 10:54:39 1998 +0200
     1.3 @@ -141,9 +141,9 @@
     1.4      ancestor.
     1.5    - The specific <typename>.induct_tac no longer exists - use the
     1.6      generic induct_tac instead.
     1.7 -  - natE has been renamed to nat.exhaustion - use exhaust_tac
     1.8 +  - natE has been renamed to nat.exhaust - use exhaust_tac
     1.9      instead of res_inst_tac ... natE. Note that the variable
    1.10 -    names in nat.exhaustion differ from the names in natE, this
    1.11 +    names in nat.exhaust differ from the names in natE, this
    1.12      may cause some "fragile" proofs to fail.
    1.13    - The theorems split_<typename>_case and split_<typename>_case_asm
    1.14      have been renamed to <typename>.split and <typename>.split_asm.