src/HOL/Nat.thy
changeset 20380 14f9f2a1caa6
parent 20355 50aaae6ae4db
child 20588 c847c56edf0c
     1.1 --- a/src/HOL/Nat.thy	Mon Aug 14 13:46:05 2006 +0200
     1.2 +++ b/src/HOL/Nat.thy	Mon Aug 14 13:46:06 2006 +0200
     1.3 @@ -1047,10 +1047,4 @@
     1.4    "1 = Suc 0"
     1.5    by simp
     1.6  
     1.7 -code_alias
     1.8 -  "nat" "Nat.nat"
     1.9 -  "0" "Nat.Zero"
    1.10 -  "1" "Nat.One"
    1.11 -  "Suc" "Nat.Suc"
    1.12 -
    1.13  end