for extraction -- use the exhaust rule that's registered with 'datatype_realizer.ML'
authorblanchet
Wed Feb 12 08:37:28 2014 +0100 (2014-02-12)
changeset 5542307dea66779f3
parent 55422 6445a05a1234
child 55424 9ab4129a76a3
for extraction -- use the exhaust rule that's registered with 'datatype_realizer.ML'
src/HOL/Nat.thy
     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 *}