# HG changeset patch
# User nipkow
# Date 1262509283 -3600
# Node ID 156c42518cfcca3b86ef54cbdf5c818e6ffbe48d
# Parent  36a2a3029fd3ed1906aa7dfe19b48aa443607d70
removed more asm_rl's - unfortunately slowdown of 1 min.

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