--- a/src/HOLCF/IOA/Modelcheck/MuIOAOracle.thy Fri Mar 20 17:04:44 2009 +0100
+++ b/src/HOLCF/IOA/Modelcheck/MuIOAOracle.thy Fri Mar 20 17:12:37 2009 +0100
@@ -18,18 +18,18 @@
(* is_sim_tac makes additionally to call_sim_tac some simplifications,
which are suitable for implementation realtion formulas *)
-fun is_sim_tac thm_list = SUBGOAL (fn (goal, i) =>
+fun is_sim_tac ss thm_list = SUBGOAL (fn (goal, i) =>
EVERY [REPEAT (etac thin_rl i),
- simp_tac (simpset() addsimps [ioa_implements_def]) i,
+ simp_tac (ss addsimps [ioa_implements_def]) i,
rtac conjI i,
rtac conjI (i+1),
TRY(call_sim_tac thm_list (i+2)),
TRY(atac (i+2)),
REPEAT(rtac refl (i+2)),
- simp_tac (simpset() addsimps (thm_list @
+ simp_tac (ss addsimps (thm_list @
comp_simps @ restrict_simps @ hide_simps @
rename_simps @ ioa_simps @ asig_simps)) (i+1),
- simp_tac (simpset() addsimps (thm_list @
+ simp_tac (ss addsimps (thm_list @
comp_simps @ restrict_simps @ hide_simps @
rename_simps @ ioa_simps @ asig_simps)) (i)]);