--- a/src/HOL/Hoare_Parallel/Gar_Coll.thy Sat Jan 02 23:18:58 2010 +0100
+++ b/src/HOL/Hoare_Parallel/Gar_Coll.thy Sun Jan 03 10:01:23 2010 +0100
@@ -1,4 +1,3 @@
-
header {* \section{The Single Mutator Case} *}
theory Gar_Coll imports Graph OG_Syntax begin
@@ -203,12 +202,11 @@
apply clarify
apply simp
apply(subgoal_tac "ind x = length (E x)")
- apply (rotate_tac -1)
- apply (simp (asm_lr))
+ apply (simp)
apply(drule Graph1)
apply simp
- apply clarify
- apply(erule allE, erule impE, assumption)
+ apply clarify
+ apply(erule allE, erule impE, assumption)
apply force
apply force
apply arith
@@ -318,12 +316,11 @@
apply clarify
apply simp
apply(subgoal_tac "ind x = length (E x)")
- apply (rotate_tac -1)
- apply (simp (asm_lr))
+ apply (simp)
apply(drule Graph1)
apply simp
apply clarify
- apply(erule allE, erule impE, assumption)
+ apply(erule allE, erule impE, assumption)
apply force
apply force
apply arith