src/HOL/Nat.thy
changeset 55423 07dea66779f3
parent 55417 01fbfb60c33e
child 55424 9ab4129a76a3
     1.1 --- a/src/HOL/Nat.thy	Wed Feb 12 08:37:28 2014 +0100
     1.2 +++ b/src/HOL/Nat.thy	Wed Feb 12 08:37:28 2014 +0100
     1.3 @@ -132,7 +132,7 @@
     1.4  lemma nat_exhaust [case_names 0 Suc, cases type: nat]:
     1.5    -- {* for backward compatibility -- names of variables differ *}
     1.6    "(y = 0 \<Longrightarrow> P) \<Longrightarrow> (\<And>nat. y = Suc nat \<Longrightarrow> P) \<Longrightarrow> P"
     1.7 -by (rule nat.exhaust)
     1.8 +by (rule old.nat.exhaust)
     1.9  
    1.10  lemma nat_induct [case_names 0 Suc, induct type: nat]:
    1.11    -- {* for backward compatibility -- names of variables differ *}