Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/HoareParallel/Gar_Coll.thy
changeset 13601 fd3e3d6b37b2
parent 13187 e5434b822a96
child 13624 17684cf64fda 
--- a/src/HOL/HoareParallel/Gar_Coll.thy	Mon Sep 30 16:12:16 2002 +0200
+++ b/src/HOL/HoareParallel/Gar_Coll.thy	Mon Sep 30 16:14:02 2002 +0200
@@ -203,7 +203,7 @@
 apply simp
 apply(subgoal_tac "ind x = length (E x)")
  apply (rotate_tac -1)
- apply simp
+ apply (simp (asm_lr))
  apply(drule Graph1)
    apply simp
   apply clarify  
@@ -320,7 +320,7 @@
 apply simp
 apply(subgoal_tac "ind x = length (E x)")
  apply (rotate_tac -1)
- apply simp
+ apply (simp (asm_lr))
  apply(drule Graph1)
    apply simp
   apply clarify  
@@ -555,12 +555,6 @@
  apply (force simp add:BtoW_def)
 apply(erule Graph4)
    apply simp+
-  apply (simp add:BtoW_def)
-  apply force
- apply (simp add:BtoW_def)
- apply force
-apply (simp add:BtoW_def)
-apply force
 --{* 7 subgoals left *}
 apply(clarify, simp add:abbrev Graph6 Graph12)
 apply(erule conjE)+
@@ -573,12 +567,6 @@
  apply (force simp add:BtoW_def)
 apply(erule Graph4)
    apply simp+
-  apply (simp add:BtoW_def)
-  apply force
- apply (simp add:BtoW_def)
- apply force
-apply (simp add:BtoW_def)
-apply force
 --{* 6 subgoals left *}
 apply(clarify, simp add:abbrev Graph6 Graph12)
 apply(erule conjE)+
@@ -592,12 +580,6 @@
   apply (force simp add:BtoW_def)
  apply(erule Graph4)
     apply simp+
-   apply (simp add:BtoW_def)
-   apply force
-  apply (simp add:BtoW_def)
-  apply force
- apply (simp add:BtoW_def)
- apply force
 apply(simp add:BtoW_def nth_list_update) 
 apply force
 --{* 5 subgoals left *}
@@ -614,12 +596,6 @@
   apply (force simp add:BtoW_def)
  apply(erule Graph4)
     apply simp+
-   apply (simp add:BtoW_def)
-   apply force
-  apply (simp add:BtoW_def)
-  apply force
- apply (simp add:BtoW_def)
- apply force
 apply(rule conjI)
  apply(simp add:nth_list_update)
  apply force
@@ -646,14 +622,6 @@
  apply (force simp add:BtoW_def)
 apply(erule Graph4)
    apply simp+
-  apply (simp add:BtoW_def)
-  apply force
- apply (simp add:BtoW_def)
- apply force
-apply (simp add:BtoW_def)
-apply force
---{* 1 subgoal left *}
-apply(simp add:abbrev)
 done
 
 lemma interfree_Redirect_Edge_Propagate_Black:
isabelle