# HG changeset patch
# User wenzelm
# Date 1301431016 -7200
# Node ID 478bdcea240a3818d8ed232f70da2befe9fc9b5f
# Parent  fa108629d13294ab16218592fb7e9a01320a685f
tuned proofs;

diff -r fa108629d132 -r 478bdcea240a src/HOL/Hoare/Examples.thy
--- a/src/HOL/Hoare/Examples.thy	Tue Mar 29 21:48:01 2011 +0200
+++ b/src/HOL/Hoare/Examples.thy	Tue Mar 29 22:36:56 2011 +0200
@@ -90,7 +90,7 @@
  {c = A^B}"
 apply vcg_simp
 apply(case_tac "b")
- apply(simp add: mod_less)
+ apply simp
 apply simp
 done
 
diff -r fa108629d132 -r 478bdcea240a src/HOL/Hoare/ExamplesAbort.thy
--- a/src/HOL/Hoare/ExamplesAbort.thy	Tue Mar 29 21:48:01 2011 +0200
+++ b/src/HOL/Hoare/ExamplesAbort.thy	Tue Mar 29 22:36:56 2011 +0200
@@ -14,8 +14,7 @@
 lemma
  "VARS a i j
  {k <= length a & i < k & j < k} j < length a \<rightarrow> a[i] := a!j {True}"
-apply vcg_simp
-done
+by vcg_simp
 
 lemma "VARS (a::int list) i
  {True}
@@ -24,7 +23,6 @@
  INV {i <= length a}
  DO a[i] := 7; i := i+1 OD
  {True}"
-apply vcg_simp
-done
+by vcg_simp
 
 end
diff -r fa108629d132 -r 478bdcea240a src/HOL/Hoare/SchorrWaite.thy
--- a/src/HOL/Hoare/SchorrWaite.thy	Tue Mar 29 21:48:01 2011 +0200
+++ b/src/HOL/Hoare/SchorrWaite.thy	Tue Mar 29 22:36:56 2011 +0200
@@ -40,7 +40,7 @@
 done
 
 lemma still_reachable: "\<lbrakk>B\<subseteq>Ra\<^sup>*``A; \<forall> (x,y) \<in> Rb-Ra. y\<in> (Ra\<^sup>*``A)\<rbrakk> \<Longrightarrow> Rb\<^sup>* `` B \<subseteq> Ra\<^sup>* `` A "
-apply (clarsimp simp only:Image_iff intro:subsetI)
+apply (clarsimp simp only:Image_iff)
 apply (erule rtrancl_induct)
  apply blast
 apply (subgoal_tac "(y, z) \<in> Ra\<union>(Rb-Ra)")