src/HOL/Nat.thy
changeset 57983 6edc3529bb4e
parent 57952 1a9a6dfc255f
child 58189 9d714be4f028
     1.1 --- a/src/HOL/Nat.thy	Mon Aug 18 15:03:25 2014 +0200
     1.2 +++ b/src/HOL/Nat.thy	Mon Aug 18 17:19:58 2014 +0200
     1.3 @@ -132,9 +132,9 @@
     1.4    nat.collapse
     1.5    nat.expand
     1.6    nat.sel
     1.7 -  nat.sel_exhaust
     1.8 -  nat.sel_split
     1.9 -  nat.sel_split_asm
    1.10 +  nat.exhaust_sel
    1.11 +  nat.split_sel
    1.12 +  nat.split_sel_asm
    1.13  
    1.14  lemma nat_exhaust [case_names 0 Suc, cases type: nat]:
    1.15    -- {* for backward compatibility -- names of variables differ *}