# HG changeset patch # User wenzelm # Date 970491544 -7200 # Node ID 98ddd0138cbf98b7a0d76746b3378ac1a445bfed # Parent 86269867de34f6e4b1c52cb08635c55f4a66cf9e delcongs weak_case_congs; diff -r 86269867de34 -r 98ddd0138cbf src/HOLCF/IOA/Modelcheck/MuIOA.ML --- a/src/HOLCF/IOA/Modelcheck/MuIOA.ML Mon Oct 02 14:58:39 2000 +0200 +++ b/src/HOLCF/IOA/Modelcheck/MuIOA.ML Mon Oct 02 14:59:04 2000 +0200 @@ -164,6 +164,8 @@ fun mk_sim_oracle (sign, SimOracleExn (subgoal,thl)) = (let + val weak_case_congs = DatatypePackage.weak_case_congs_of_sg sign; + val concl = (Logic.strip_imp_concl subgoal); val ic_str = delete_ul_string(Sign.string_of_term sign (IntC sign concl)); @@ -258,12 +260,14 @@ 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() delcongs [if_weak_cong] +by (full_simp_tac ((simpset() delcongs (if_weak_cong :: weak_case_congs) 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 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 (full_simp_tac + (Mucke_ss delcongs (if_weak_cong :: weak_case_congs) delsimps [not_iff,split_part]) 1); +by (REPEAT (if_full_simp_tac + (simpset() delcongs (if_weak_cong :: weak_case_congs) 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);