src/HOL/IOA/Solve.ML

 by (res_inst_tac [("x",
    "(filter_oseq (%a. a:actions(asig_of(C1))) \
 \                (fst ex),                                                \
 \    %i. fst (snd ex i))")]  bexI 1);
 (* fst(s) is in projected execution *)
- by (Simp_tac 1);
- by (fast_tac (claset() delSWrapper"split_all_tac")1);
+ by (Force_tac 1);
 (* projected execution is indeed an execution *)
 by (asm_full_simp_tac
-      (simpset() addsimps [executions_def,is_execution_fragment_def,
-                          par_def,starts_of_def,trans_of_def,filter_oseq_def]
-                addsplits [option.split]) 1);
+      (simpset() delcongs [if_weak_cong]
+		 addsimps [executions_def,is_execution_fragment_def,
+			   par_def,starts_of_def,trans_of_def,filter_oseq_def]
+                 addsplits [option.split]) 1);
 qed"comp1_reachable";
 
 
 (* Exact copy of proof of comp1_reachable for the second 
    component of a parallel composition.     *)

 by (res_inst_tac [("x",
    "(filter_oseq (%a. a:actions(asig_of(C2)))\
 \                (fst ex),                                                \
 \    %i. snd (snd ex i))")]  bexI 1);
 (* fst(s) is in projected execution *)
- by (Simp_tac 1);
- by (fast_tac (claset() delSWrapper"split_all_tac")1);
+ by (Force_tac 1);
 (* projected execution is indeed an execution *)
 by (asm_full_simp_tac
-      (simpset() addsimps [executions_def,is_execution_fragment_def,
-                          par_def,starts_of_def,trans_of_def,filter_oseq_def]
-                addsplits [option.split]) 1);
+      (simpset() delcongs [if_weak_cong]
+		 addsimps [executions_def,is_execution_fragment_def,
+			   par_def,starts_of_def,trans_of_def,filter_oseq_def]
+                 addsplits [option.split]) 1);
 qed"comp2_reachable";
 
-Delsplits [split_if];
-
-(* Composition of possibility-mappings *)
-Goalw [is_weak_pmap_def] "[| is_weak_pmap f C1 A1 & \
-\               externals(asig_of(A1))=externals(asig_of(C1)) &\
-\               is_weak_pmap g C2 A2 &  \
-\               externals(asig_of(A2))=externals(asig_of(C2)) & \
-\               compat_ioas C1 C2 & compat_ioas A1 A2  |]     \
+Delsplits [split_if]; Delcongs [if_weak_cong];
+
+(* THIS THEOREM IS NEVER USED (lcp)
+   Composition of possibility-mappings *)
+Goalw [is_weak_pmap_def]
+     "[| is_weak_pmap f C1 A1; \
+\        externals(asig_of(A1))=externals(asig_of(C1));\
+\        is_weak_pmap g C2 A2;  \
+\        externals(asig_of(A2))=externals(asig_of(C2)); \
+\        compat_ioas C1 C2; compat_ioas A1 A2  |]     \
 \  ==> is_weak_pmap (%p.(f(fst(p)),g(snd(p)))) (C1||C2) (A1||A2)";
  by (rtac conjI 1);
 (* start_states *)
  by (asm_full_simp_tac (simpset() addsimps [par_def, starts_of_def]) 1);
 (* transitions *)
 by (REPEAT (rtac allI 1));
 by (rtac imp_conj_lemma 1);
-by (REPEAT(etac conjE 1));
 by (simp_tac (simpset() addsimps [externals_of_par_extra]) 1);
 by (simp_tac (simpset() addsimps [par_def]) 1);
 by (asm_full_simp_tac (simpset() addsimps [trans_of_def]) 1);
 by (stac split_if 1);
 by (rtac conjI 1);

 by (Asm_full_simp_tac 2);
 by (Fast_tac 2);
 by (simp_tac (simpset() addsimps [conj_disj_distribR] addcongs [conj_cong]
                  addsplits [split_if]) 1);
 by (REPEAT((resolve_tac [conjI,impI] 1 ORELSE etac conjE 1) THEN
-        asm_full_simp_tac(simpset() addsimps[comp1_reachable,
-                                      comp2_reachable])1));
+	   asm_full_simp_tac(simpset() addsimps[comp1_reachable,
+						comp2_reachable])1));
 qed"fxg_is_weak_pmap_of_product_IOA";
 
 
 Goal "[| reachable (rename C g) s |] ==> reachable C s";
 by (asm_full_simp_tac (simpset() addsimps [reachable_def]) 1); 

 by (cut_inst_tac [("C","C"),("g","g"),("s","s")] reachable_rename_ioa 1);
 by Auto_tac;
 qed"rename_through_pmap";
 
 Addsplits [split_if];
+Addcongs  [if_weak_cong];