removed more asm_rl's - unfortunately slowdown of 1 min.
--- 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
--- a/src/HOL/Hoare_Parallel/OG_Examples.thy Sat Jan 02 23:18:58 2010 +0100
+++ b/src/HOL/Hoare_Parallel/OG_Examples.thy Sun Jan 03 10:01:23 2010 +0100
@@ -1,4 +1,3 @@
-
header {* \section{Examples} *}
theory OG_Examples imports OG_Syntax begin
@@ -434,16 +433,14 @@
apply(tactic {* ALLGOALS (clarify_tac @{claset}) *})
--{* 112 subgoals left *}
apply(simp_all (no_asm))
+--{* 97 subgoals left *}
apply(tactic {*ALLGOALS (conjI_Tac (K all_tac)) *})
--{* 930 subgoals left *}
apply(tactic {* ALLGOALS (clarify_tac @{claset}) *})
-apply(simp_all (asm_lr) only:length_0_conv [THEN sym])
---{* 44 subgoals left *}
-apply (simp_all (asm_lr) del:length_0_conv add: neq0_conv nth_list_update mod_less_divisor mod_lemma)
---{* 32 subgoals left *}
-apply(tactic {* ALLGOALS (clarify_tac @{claset}) *})
-
-apply(tactic {* TRYALL (Lin_Arith.tac @{context}) *})
+--{* 99 subgoals left *}
+apply(simp_all (*asm_lr*) only:length_0_conv [THEN sym])
+--{* 20 subgoals left *}
+apply (simp_all (*asm_lr*) del:length_0_conv length_greater_0_conv add: nth_list_update mod_lemma)
--{* 9 subgoals left *}
apply (force simp add:less_Suc_eq)
apply(drule sym)
--- a/src/HOL/Hoare_Parallel/RG_Examples.thy Sat Jan 02 23:18:58 2010 +0100
+++ b/src/HOL/Hoare_Parallel/RG_Examples.thy Sun Jan 03 10:01:23 2010 +0100
@@ -120,12 +120,11 @@
apply clarify
apply simp
apply(subgoal_tac "j=0")
- apply (rotate_tac -1)
- apply (simp (asm_lr))
+ apply (simp)
apply arith
apply clarify
apply(case_tac i,simp,simp)
- apply clarify
+ apply clarify
apply simp
apply(erule_tac x=0 in all_dupE)
apply(erule_tac x=1 in allE,simp)