--- a/src/HOL/IOA/Solve.thy Tue Aug 09 23:29:54 2016 +0200
+++ b/src/HOL/IOA/Solve.thy Wed Aug 10 09:33:54 2016 +0200
@@ -86,7 +86,7 @@
apply (simp cong del: if_weak_cong
add: executions_def is_execution_fragment_def par_def starts_of_def
trans_of_def filter_oseq_def
- split add: option.split)
+ split: option.split)
done
@@ -103,7 +103,7 @@
apply (simp cong del: if_weak_cong
add: executions_def is_execution_fragment_def par_def starts_of_def
trans_of_def filter_oseq_def
- split add: option.split)
+ split: option.split)
done
declare if_split [split del] if_weak_cong [cong del]
@@ -143,7 +143,7 @@
(* delete auxiliary subgoal *)
prefer 2
apply force
- apply (simp (no_asm) add: conj_disj_distribR cong add: conj_cong split add: if_split)
+ apply (simp (no_asm) add: conj_disj_distribR cong add: conj_cong split: if_split)
apply (tactic \<open>
REPEAT((resolve_tac @{context} [conjI, impI] 1 ORELSE eresolve_tac @{context} [conjE] 1) THEN
asm_full_simp_tac(@{context} addsimps [@{thm comp1_reachable}, @{thm comp2_reachable}]) 1)\<close>)
@@ -157,7 +157,7 @@
apply (simp (no_asm))
(* execution is indeed an execution of C *)
apply (simp add: executions_def is_execution_fragment_def par_def
- starts_of_def trans_of_def rename_def split add: option.split)
+ starts_of_def trans_of_def rename_def split: option.split)
apply force
done
@@ -197,7 +197,7 @@
apply assumption
apply simp
(* x is internal *)
- apply (simp (no_asm) add: de_Morgan_disj de_Morgan_conj not_ex cong add: conj_cong)
+ apply (simp (no_asm) cong add: conj_cong)
apply (rule impI)
apply (erule conjE)
apply (cut_tac C = "C" and g = "g" and s = "s" in reachable_rename_ioa)