src/HOL/Arith.ML
changeset 3724 f33e301a89f5
parent 3718 d78cf498a88c
child 3842 b55686a7b22c
     1.1 --- a/src/HOL/Arith.ML	Mon Sep 29 11:36:44 1997 +0200
     1.2 +++ b/src/HOL/Arith.ML	Mon Sep 29 11:37:02 1997 +0200
     1.3 @@ -403,7 +403,7 @@
     1.4  Addsimps [diff_add_inverse2];
     1.5  
     1.6  goal Arith.thy "!!i j k::nat. i<=j ==> (j-i=k) = (j=k+i)";
     1.7 -by (Step_tac 1);
     1.8 +by Safe_tac;
     1.9  by (ALLGOALS Asm_simp_tac);
    1.10  qed "le_imp_diff_is_add";
    1.11  
    1.12 @@ -546,7 +546,7 @@
    1.13  
    1.14  goal Arith.thy "!!k. 0<k ==> (m*k = n*k) = (m=n)";
    1.15  by (cut_facts_tac [less_linear] 1);
    1.16 -by (Step_tac 1);
    1.17 +by Safe_tac;
    1.18  by (assume_tac 2);
    1.19  by (ALLGOALS (dtac mult_less_mono1 THEN' assume_tac));
    1.20  by (ALLGOALS Asm_full_simp_tac);