--- a/src/HOLCF/IOA/Modelcheck/MuIOA.ML Fri Aug 20 15:44:29 1999 +0200
+++ b/src/HOLCF/IOA/Modelcheck/MuIOA.ML Fri Aug 20 16:16:02 1999 +0200
@@ -258,11 +258,12 @@
by (REPEAT (rtac impI 1));
by (REPEAT (dtac eq_reflection 1));
(* Bis hierher wird im Kapitel 4 erl"autert, ab hier im Kapitel 5 *)
-by (full_simp_tac ((simpset() delsimps [not_iff,split_part])
+by (full_simp_tac ((simpset() delcongs [if_weak_cong]
+ delsimps [not_iff,split_part])
addsimps (thl @ comp_simps @ restrict_simps @ hide_simps @
rename_simps @ ioa_simps @ asig_simps)) 1);
-by (full_simp_tac (Mucke_ss delsimps [not_iff,split_part]) 1);
-by (REPEAT (if_full_simp_tac (simpset() delsimps [not_iff,split_part]) 1));
+by (full_simp_tac (Mucke_ss delcongs [if_weak_cong] delsimps [not_iff,split_part]) 1);
+by (REPEAT (if_full_simp_tac (simpset() delcongs [if_weak_cong] delsimps [not_iff,split_part]) 1));
by (call_mucke_tac 1);
(* Bis hierher wird im Kapitel 5 erl"autert, ab hier wieder im Kapitel 4 *)
by (atac 1);