src/HOL/Library/Extended_Nat.thy
changeset 58306 117ba6cbe414
parent 57514 bdc2c6b40bf2
child 58881 b9556a055632
     1.1 --- a/src/HOL/Library/Extended_Nat.thy	Thu Sep 11 18:54:36 2014 +0200
     1.2 +++ b/src/HOL/Library/Extended_Nat.thy	Thu Sep 11 18:54:36 2014 +0200
     1.3 @@ -44,7 +44,7 @@
     1.4      by (rule exI[of _ "to_nat \<circ> Rep_enat"]) (simp add: inj_on_def Rep_enat_inject)
     1.5  qed
     1.6   
     1.7 -rep_datatype enat "\<infinity> :: enat"
     1.8 +old_rep_datatype enat "\<infinity> :: enat"
     1.9  proof -
    1.10    fix P i assume "\<And>j. P (enat j)" "P \<infinity>"
    1.11    then show "P i"