src/HOL/Nat.ML
changeset 15413 901d1bfedf09
parent 15341 254f6f00b60e
child 15921 b6e345548913
     1.1 --- a/src/HOL/Nat.ML	Wed Dec 15 10:19:19 2004 +0100
     1.2 +++ b/src/HOL/Nat.ML	Wed Dec 15 17:32:40 2004 +0100
     1.3 @@ -110,9 +110,7 @@
     1.4  val gr0I = thm "gr0I";
     1.5  val gr0_conv_Suc = thm "gr0_conv_Suc";
     1.6  val gr_implies_not0 = thm "gr_implies_not0";
     1.7 -val inj_Rep_Nat = thm "inj_Rep_Nat";
     1.8  val inj_Suc = thm "inj_Suc";
     1.9 -val inj_on_Abs_Nat = thm "inj_on_Abs_Nat";
    1.10  val le0 = thm "le0";
    1.11  val leD = thm "leD";
    1.12  val leE = thm "leE";