1.1 --- a/src/HOL/Hoare/Examples.ML	Wed Aug 19 10:27:49 1998 +0200
     1.2 +++ b/src/HOL/Hoare/Examples.ML	Wed Aug 19 10:28:25 1998 +0200
     1.3 @@ -36,13 +36,12 @@
     1.4  
     1.5  by (hoare_tac 1);
     1.6  (*Now prove the verification conditions*)
     1.7 -by Safe_tac;
     1.8 -by (etac less_imp_diff_positive 1);
     1.9 +by Auto_tac;
    1.10 +by (etac gcd_nnn 4);
    1.11 +by (asm_full_simp_tac (simpset() addsimps [not_less_iff_le, gcd_diff_l]) 3);
    1.12 +by (force_tac (claset(),
    1.13 +	       simpset() addsimps [not_less_iff_le, le_eq_less_or_eq]) 2);
    1.14  by (asm_simp_tac (simpset() addsimps [less_imp_le, gcd_diff_r]) 1);
    1.15 -by (asm_full_simp_tac (simpset() addsimps [not_less_iff_le, gcd_diff_l]) 2);
    1.16 -by (etac gcd_nnn 2);
    1.17 -by (full_simp_tac (simpset() addsimps [not_less_iff_le, le_eq_less_or_eq]) 1);
    1.18 -by (blast_tac (claset() addIs [less_imp_diff_positive]) 1);
    1.19  qed "Euclid_GCD";
    1.20  
    1.21