src/HOL/Hoare/Examples.ML
changeset 4153 e534c4c32d54
parent 4089 96fba19bcbe2
child 4356 0dfd34f0d33d
     1.1 --- a/src/HOL/Hoare/Examples.ML	Wed Nov 05 13:14:15 1997 +0100
     1.2 +++ b/src/HOL/Hoare/Examples.ML	Wed Nov 05 13:23:46 1997 +0100
     1.3 @@ -36,7 +36,7 @@
     1.4  
     1.5  by (hoare_tac 1);
     1.6  (*Now prove the verification conditions*)
     1.7 -by (safe_tac (claset()));
     1.8 +by Safe_tac;
     1.9  by (etac less_imp_diff_positive 1);
    1.10  by (asm_simp_tac (simpset() addsimps [less_imp_le, gcd_diff_r]) 1);
    1.11  by (asm_full_simp_tac (simpset() addsimps [not_less_iff_le, gcd_diff_l]) 2);
    1.12 @@ -67,7 +67,7 @@
    1.13  
    1.14  by (simp_tac ((simpset_of Arith.thy) addsimps [pow_0]) 3);
    1.15  
    1.16 -by (safe_tac (claset()));
    1.17 +by Safe_tac;
    1.18  
    1.19  by (subgoal_tac "a*a=a pow 2" 1);
    1.20  by (Asm_simp_tac 1);
    1.21 @@ -103,7 +103,7 @@
    1.22  \ {b = fac A}";
    1.23  
    1.24  by (hoare_tac 1);
    1.25 -by (safe_tac (claset()));
    1.26 +by Safe_tac;
    1.27  by (res_inst_tac [("n","a")] natE 1);
    1.28  by (ALLGOALS
    1.29      (asm_simp_tac