src/HOL/Nat.ML
changeset 9108 9fff97d29837
parent 8942 6aad5381ba83
child 9436 62bb04ab4b01
     1.1 --- a/src/HOL/Nat.ML	Thu Jun 22 11:37:13 2000 +0200
     1.2 +++ b/src/HOL/Nat.ML	Thu Jun 22 23:04:34 2000 +0200
     1.3 @@ -7,6 +7,8 @@
     1.4  (** conversion rules for nat_rec **)
     1.5  
     1.6  val [nat_rec_0, nat_rec_Suc] = nat.recs;
     1.7 +bind_thm ("nat_rec_0", nat_rec_0);
     1.8 +bind_thm ("nat_rec_Suc", nat_rec_Suc);
     1.9  
    1.10  (*These 2 rules ease the use of primitive recursion.  NOTE USE OF == *)
    1.11  val prems = Goal
    1.12 @@ -20,6 +22,8 @@
    1.13  qed "def_nat_rec_Suc";
    1.14  
    1.15  val [nat_case_0, nat_case_Suc] = nat.cases;
    1.16 +bind_thm ("nat_case_0", nat_case_0);
    1.17 +bind_thm ("nat_case_Suc", nat_case_Suc);
    1.18  
    1.19  Goal "n ~= 0 ==> EX m. n = Suc m";
    1.20  by (case_tac "n" 1);