src/HOL/Library/Efficient_Nat.thy
changeset 24423 ae9cd0e92423
parent 24222 a8a28c15c5cc
child 24630 351a308ab58d
     1.1 --- a/src/HOL/Library/Efficient_Nat.thy	Fri Aug 24 14:14:18 2007 +0200
     1.2 +++ b/src/HOL/Library/Efficient_Nat.thy	Fri Aug 24 14:14:20 2007 +0200
     1.3 @@ -63,6 +63,8 @@
     1.4  lemma eq_nat_of_int: "int' n = x \<Longrightarrow> n = nat_of_int x"
     1.5  by (erule subst, simp only: nat_of_int_int)
     1.6  
     1.7 +code_datatype nat_of_int
     1.8 +
     1.9  text {*
    1.10    Case analysis on natural numbers is rephrased using a conditional
    1.11    expression:
    1.12 @@ -161,8 +163,6 @@
    1.13    @{typ nat} is no longer a datatype but embedded into the integers.
    1.14  *}
    1.15  
    1.16 -code_datatype nat_of_int
    1.17 -
    1.18  code_type nat
    1.19    (SML "IntInf.int")
    1.20    (OCaml "Big'_int.big'_int")