--- a/src/HOLCF/IOA/Modelcheck/Cockpit.thy Fri Mar 20 17:04:44 2009 +0100
+++ b/src/HOLCF/IOA/Modelcheck/Cockpit.thy Fri Mar 20 17:12:37 2009 +0100
@@ -102,18 +102,18 @@
(* to prove, that info is always set at the recent alarm *)
lemma cockpit_implements_Info_while_Al: "cockpit =<| Info_while_Al"
-apply (tactic {* is_sim_tac (thms "aut_simps") 1 *})
+apply (tactic {* is_sim_tac @{simpset} (thms "aut_simps") 1 *})
done
(* to prove that before any alarm arrives (and after each acknowledgment),
info remains at None *)
lemma cockpit_implements_Info_before_Al: "cockpit =<| Info_before_Al"
-apply (tactic {* is_sim_tac (thms "aut_simps") 1 *})
+apply (tactic {* is_sim_tac @{simpset} (thms "aut_simps") 1 *})
done
(* to prove that before any alarm would be acknowledged, it must be arrived *)
lemma cockpit_implements_Al_before_Ack: "cockpit_hide =<| Al_before_Ack"
-apply (tactic {* is_sim_tac (thms "aut_simps") 1 *})
+apply (tactic {* is_sim_tac @{simpset} (thms "aut_simps") 1 *})
apply auto
done