# HG changeset patch
# User wenzelm
# Date 935158562 -7200
# Node ID 838a7bc92d814b649bf2890b85db466d70b476b8
# Parent  e01aab03a2a12782942a691f3b073566b8afef28
delcongs [if_weak_cong];

diff -r e01aab03a2a1 -r 838a7bc92d81 src/HOLCF/IOA/Modelcheck/MuIOA.ML
--- 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);