--- a/src/HOL/HoareParallel/Mul_Gar_Coll.thy Thu May 30 10:12:11 2002 +0200
+++ b/src/HOL/HoareParallel/Mul_Gar_Coll.thy Thu May 30 10:12:52 2002 +0200
@@ -93,7 +93,6 @@
apply interfree_aux
apply safe
apply(simp_all add: nth_list_update)
-apply force+
done
lemma Mul_interfree_Redirect_Edge_Color_Target:
@@ -112,7 +111,6 @@
apply interfree_aux
apply safe
apply(simp_all add:nth_list_update)
-apply (drule not_sym,force)+
done
lemma Mul_interfree_Color_Target_Color_Target:
@@ -122,7 +120,6 @@
apply interfree_aux
apply safe
apply(simp_all add: nth_list_update)
-apply (drule not_sym,force)
done
lemmas mul_mutator_interfree =
@@ -138,7 +135,6 @@
apply(tactic {* TRYALL (interfree_aux_tac) *})
apply(tactic {* ALLGOALS Clarify_tac *})
apply (simp_all add:nth_list_update)
-apply force+
done
subsubsection {* Modular Parameterized Mutators *}
@@ -154,7 +150,7 @@
apply oghoare
apply(force simp add:Mul_Mutator_def mul_mutator_defs nth_list_update)
apply(erule Mul_Mutator)
-apply(simp add:Mul_interfree_Mutator_Mutator)
+apply(simp add:Mul_interfree_Mutator_Mutator)
apply(force simp add:Mul_Mutator_def mul_mutator_defs nth_list_update)
done
@@ -204,8 +200,6 @@
apply(simp_all add:mul_collector_defs Graph_defs)
apply safe
apply(simp_all add:nth_list_update)
- apply (erule less_SucE)
- apply simp+
apply (erule less_SucE)
apply simp+
apply(drule le_imp_less_or_eq)
@@ -1288,4 +1282,4 @@
apply(simp add:Mul_Mutator_def mul_mutator_defs mul_collector_defs nth_append)
done
-end
\ No newline at end of file
+end