NEWS
changeset 5226 89934cd022a9
parent 5217 3ecd7c952396
child 5251 fee54d5c511c
     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.