--- a/src/HOL/TLA/Inc/Inc.thy Tue Apr 16 17:54:14 2013 +0200
+++ b/src/HOL/TLA/Inc/Inc.thy Thu Apr 18 17:07:01 2013 +0200
@@ -170,9 +170,9 @@
--> (pc1 = #g ~> pc1 = #a)"
apply (rule SF1)
apply (tactic
- {* action_simp_tac (@{simpset} addsimps @{thms Psi_defs}) [] [@{thm squareE}] 1 *})
+ {* action_simp_tac (@{context} addsimps @{thms Psi_defs}) [] [@{thm squareE}] 1 *})
apply (tactic
- {* action_simp_tac (@{simpset} addsimps @{thm angle_def} :: @{thms Psi_defs}) [] [] 1 *})
+ {* action_simp_tac (@{context} addsimps @{thm angle_def} :: @{thms Psi_defs}) [] [] 1 *})
(* reduce |- []A --> <>Enabled B to |- A --> Enabled B *)
apply (auto intro!: InitDmd_gen [temp_use] N1_enabled_at_g [temp_use]
dest!: STL2_gen [temp_use] simp: Init_def)
@@ -191,8 +191,8 @@
"|- [][(N1 | N2) & ~beta1]_(x,y,sem,pc1,pc2) & SF(N2)_(x,y,sem,pc1,pc2) & []#True
--> (pc2 = #g ~> pc2 = #a)"
apply (rule SF1)
- apply (tactic {* action_simp_tac (@{simpset} addsimps @{thms Psi_defs}) [] [@{thm squareE}] 1 *})
- apply (tactic {* action_simp_tac (@{simpset} addsimps @{thm angle_def} :: @{thms Psi_defs})
+ apply (tactic {* action_simp_tac (@{context} addsimps @{thms Psi_defs}) [] [@{thm squareE}] 1 *})
+ apply (tactic {* action_simp_tac (@{context} addsimps @{thm angle_def} :: @{thms Psi_defs})
[] [] 1 *})
apply (auto intro!: InitDmd_gen [temp_use] N2_enabled_at_g [temp_use]
dest!: STL2_gen [temp_use] simp add: Init_def)
@@ -211,9 +211,9 @@
--> (pc2 = #b ~> pc2 = #g)"
apply (rule SF1)
apply (tactic
- {* action_simp_tac (@{simpset} addsimps @{thms Psi_defs}) [] [@{thm squareE}] 1 *})
+ {* action_simp_tac (@{context} addsimps @{thms Psi_defs}) [] [@{thm squareE}] 1 *})
apply (tactic
- {* action_simp_tac (@{simpset} addsimps @{thm angle_def} :: @{thms Psi_defs}) [] [] 1 *})
+ {* action_simp_tac (@{context} addsimps @{thm angle_def} :: @{thms Psi_defs}) [] [] 1 *})
apply (auto intro!: InitDmd_gen [temp_use] N2_enabled_at_b [temp_use]
dest!: STL2_gen [temp_use] simp: Init_def)
done
@@ -253,9 +253,9 @@
& SF(N1)_(x,y,sem,pc1,pc2) & [] SF(N2)_(x,y,sem,pc1,pc2)
--> (pc1 = #a ~> pc1 = #b)"
apply (rule SF1)
- apply (tactic {* action_simp_tac (@{simpset} addsimps @{thms Psi_defs}) [] [@{thm squareE}] 1 *})
+ apply (tactic {* action_simp_tac (@{context} addsimps @{thms Psi_defs}) [] [@{thm squareE}] 1 *})
apply (tactic
- {* action_simp_tac (@{simpset} addsimps (@{thm angle_def} :: @{thms Psi_defs})) [] [] 1 *})
+ {* action_simp_tac (@{context} addsimps (@{thm angle_def} :: @{thms Psi_defs})) [] [] 1 *})
apply (clarsimp intro!: N1_enabled_at_both_a [THEN DmdImpl [temp_use]])
apply (auto intro!: BoxDmd2_simple [temp_use] N2_live [temp_use]
simp: split_box_conj more_temp_simps)