diff -r 36a2a3029fd3 -r 156c42518cfc src/HOL/Hoare_Parallel/Gar_Coll.thy
--- 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