src/HOL/Nat.ML
changeset 5316 7a8975451a89
parent 5188 633ec5f6c155
child 5644 85fd64148873
     1.1 --- a/src/HOL/Nat.ML	Thu Aug 13 18:07:56 1998 +0200
     1.2 +++ b/src/HOL/Nat.ML	Thu Aug 13 18:14:26 1998 +0200
     1.3 @@ -9,12 +9,12 @@
     1.4  val [nat_rec_0, nat_rec_Suc] = nat.recs;
     1.5  
     1.6  (*These 2 rules ease the use of primitive recursion.  NOTE USE OF == *)
     1.7 -val prems = goal thy
     1.8 +val prems = Goal
     1.9      "[| !!n. f(n) == nat_rec c h n |] ==> f(0) = c";
    1.10  by (simp_tac (simpset() addsimps prems) 1);
    1.11  qed "def_nat_rec_0";
    1.12  
    1.13 -val prems = goal thy
    1.14 +val prems = Goal
    1.15      "[| !!n. f(n) == nat_rec c h n |] ==> f(Suc(n)) = h n (f n)";
    1.16  by (simp_tac (simpset() addsimps prems) 1);
    1.17  qed "def_nat_rec_Suc";
    1.18 @@ -26,9 +26,8 @@
    1.19  by (REPEAT (Blast_tac 1));
    1.20  qed "not0_implies_Suc";
    1.21  
    1.22 -val prems = goal thy "m<n ==> n ~= 0";
    1.23 +Goal "m<n ==> n ~= 0";
    1.24  by (exhaust_tac "n" 1);
    1.25 -by (cut_facts_tac prems 1);
    1.26  by (ALLGOALS Asm_full_simp_tac);
    1.27  qed "gr_implies_not0";
    1.28