src/HOL/Hoare/Examples.thy
changeset 16733 236dfafbeb63
parent 16417 9bc16273c2d4
child 16796 140f1e0ea846
     1.1 --- a/src/HOL/Hoare/Examples.thy	Thu Jul 07 12:36:56 2005 +0200
     1.2 +++ b/src/HOL/Hoare/Examples.thy	Thu Jul 07 12:39:17 2005 +0200
     1.3 @@ -73,7 +73,6 @@
     1.4  apply vcg
     1.5    apply simp
     1.6   apply(simp add: distribs gcd_diff_r not_less_iff_le gcd_diff_l)
     1.7 - apply arith
     1.8  apply(simp add: distribs gcd_nnn)
     1.9  done
    1.10  
    1.11 @@ -136,7 +135,6 @@
    1.12   DO r := r+1 OD
    1.13   {r*r <= X & X < (r+1)*(r+1)}"
    1.14  apply vcg_simp
    1.15 -apply auto
    1.16  done
    1.17  
    1.18  (* without multiplication *)
    1.19 @@ -149,7 +147,6 @@
    1.20   DO r := r + 1; w := w + u + 2; u := u + 2 OD
    1.21   {r*r <= X & X < (r+1)*(r+1)}"
    1.22  apply vcg_simp
    1.23 -apply auto
    1.24  done
    1.25  
    1.26  
    1.27 @@ -231,11 +228,10 @@
    1.28  apply (simp);
    1.29  apply (erule thin_rl)+
    1.30  apply vcg_simp
    1.31 -    apply (force simp: neq_Nil_conv)
    1.32 -   apply (blast elim!: less_SucE intro: Suc_leI)
    1.33 -  apply (blast elim!: less_SucE intro: less_imp_diff_less dest: lem)
    1.34 - apply (force simp: nth_list_update)
    1.35 -apply (auto intro: order_antisym)
    1.36 +   apply (force simp: neq_Nil_conv)
    1.37 +  apply (blast elim!: less_SucE intro: Suc_leI)
    1.38 + apply (blast elim!: less_SucE intro: less_imp_diff_less dest: lem)
    1.39 +apply (force simp: nth_list_update)
    1.40  done
    1.41  
    1.42  end
    1.43 \ No newline at end of file