src/HOL/Arith.ML
changeset 5316 7a8975451a89
parent 5270 70c599bff977
child 5329 1003ddc30299
     1.1 --- a/src/HOL/Arith.ML	Thu Aug 13 18:07:56 1998 +0200
     1.2 +++ b/src/HOL/Arith.ML	Thu Aug 13 18:14:26 1998 +0200
     1.3 @@ -221,7 +221,7 @@
     1.4  qed "add_less_mono";
     1.5  
     1.6  (*A [clumsy] way of lifting < monotonicity to <= monotonicity *)
     1.7 -val [lt_mono,le] = goal thy
     1.8 +val [lt_mono,le] = Goal
     1.9       "[| !!i j::nat. i<j ==> f(i) < f(j);       \
    1.10  \        i <= j                                 \
    1.11  \     |] ==> f(i) <= (f(j)::nat)";
    1.12 @@ -331,8 +331,8 @@
    1.13  
    1.14  (*** More results about difference ***)
    1.15  
    1.16 -val [prem] = goal thy "n < Suc(m) ==> Suc(m)-n = Suc(m-n)";
    1.17 -by (rtac (prem RS rev_mp) 1);
    1.18 +Goal "n < Suc(m) ==> Suc(m)-n = Suc(m-n)";
    1.19 +by (etac rev_mp 1);
    1.20  by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
    1.21  by (ALLGOALS Asm_simp_tac);
    1.22  qed "Suc_diff_n";
    1.23 @@ -411,20 +411,20 @@
    1.24  by (ALLGOALS Asm_simp_tac);
    1.25  qed "le_imp_diff_is_add";
    1.26  
    1.27 -val [prem] = goal thy "m < Suc(n) ==> m-n = 0";
    1.28 -by (rtac (prem RS rev_mp) 1);
    1.29 +Goal "m < Suc(n) ==> m-n = 0";
    1.30 +by (etac rev_mp 1);
    1.31  by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
    1.32  by (asm_simp_tac (simpset() addsimps [less_Suc_eq]) 1);
    1.33  by (ALLGOALS Asm_simp_tac);
    1.34  qed "less_imp_diff_is_0";
    1.35  
    1.36 -val prems = goal thy "m-n = 0  -->  n-m = 0  -->  m=n";
    1.37 +Goal "m-n = 0  -->  n-m = 0  -->  m=n";
    1.38  by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
    1.39  by (REPEAT(Simp_tac 1 THEN TRY(atac 1)));
    1.40  qed_spec_mp "diffs0_imp_equal";
    1.41  
    1.42 -val [prem] = goal thy "m<n ==> 0<n-m";
    1.43 -by (rtac (prem RS rev_mp) 1);
    1.44 +Goal "m<n ==> 0<n-m";
    1.45 +by (etac rev_mp 1);
    1.46  by (res_inst_tac [("m","m"),("n","n")] diff_induct 1);
    1.47  by (ALLGOALS Asm_simp_tac);
    1.48  qed "less_imp_diff_positive";
    1.49 @@ -448,7 +448,7 @@
    1.50  by (ALLGOALS (Clarify_tac THEN' Simp_tac THEN' TRY o Blast_tac));
    1.51  qed "zero_induct_lemma";
    1.52  
    1.53 -val prems = goal thy "[| P(k);  !!n. P(Suc(n)) ==> P(n) |] ==> P(0)";
    1.54 +val prems = Goal "[| P(k);  !!n. P(Suc(n)) ==> P(n) |] ==> P(0)";
    1.55  by (rtac (diff_self_eq_0 RS subst) 1);
    1.56  by (rtac (zero_induct_lemma RS mp RS mp) 1);
    1.57  by (REPEAT (ares_tac ([impI,allI]@prems) 1));