--- 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
--- 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
--- 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)")