src/HOL/Nat.ML
changeset 21669 c68717c16013
parent 17274 746bb4c56800
     1.1 --- a/src/HOL/Nat.ML	Tue Dec 05 22:14:53 2006 +0100
     1.2 +++ b/src/HOL/Nat.ML	Wed Dec 06 01:12:36 2006 +0100
     1.3 @@ -17,17 +17,6 @@
     1.4    val simps = thms "nat.simps";
     1.5  end;
     1.6  
     1.7 -val [nat_rec_0, nat_rec_Suc] = thms "nat.recs";
     1.8 -bind_thm ("nat_rec_0", nat_rec_0);
     1.9 -bind_thm ("nat_rec_Suc", nat_rec_Suc);
    1.10 -
    1.11 -val [nat_case_0, nat_case_Suc] = thms "nat.cases";
    1.12 -bind_thm ("nat_case_0", nat_case_0);
    1.13 -bind_thm ("nat_case_Suc", nat_case_Suc);
    1.14 -
    1.15 -val leD = thm "leD";  (*Now defined in Orderings.thy*)
    1.16 -val leI = thm "leI";
    1.17 -
    1.18  val Least_Suc = thm "Least_Suc";
    1.19  val Least_Suc2 = thm "Least_Suc2";
    1.20  val One_nat_def = thm "One_nat_def";