src/HOL/Code_Numeral.thy
changeset 58306 117ba6cbe414
parent 57512 cc97b347b301
child 58377 c6f93b8d2d8e
     1.1 --- a/src/HOL/Code_Numeral.thy	Thu Sep 11 18:54:36 2014 +0200
     1.2 +++ b/src/HOL/Code_Numeral.thy	Thu Sep 11 18:54:36 2014 +0200
     1.3 @@ -800,7 +800,7 @@
     1.4  
     1.5  declare Suc.rep_eq [simp]
     1.6  
     1.7 -rep_datatype "0::natural" Suc
     1.8 +old_rep_datatype "0::natural" Suc
     1.9    by (transfer, fact nat.induct nat.inject nat.distinct)+
    1.10  
    1.11  lemma natural_cases [case_names nat, cases type: natural]: