--- a/src/HOL/TLA/Inc/Inc.thy Sat Jan 05 17:00:43 2019 +0100
+++ b/src/HOL/TLA/Inc/Inc.thy Sat Jan 05 17:24:33 2019 +0100
@@ -170,9 +170,9 @@
\<longrightarrow> (pc1 = #g \<leadsto> pc1 = #a)"
apply (rule SF1)
apply (tactic
- \<open>action_simp_tac (@{context} addsimps @{thms Psi_defs}) [] [@{thm squareE}] 1\<close>)
+ \<open>action_simp_tac (\<^context> addsimps @{thms Psi_defs}) [] [@{thm squareE}] 1\<close>)
apply (tactic
- \<open>action_simp_tac (@{context} addsimps @{thm angle_def} :: @{thms Psi_defs}) [] [] 1\<close>)
+ \<open>action_simp_tac (\<^context> addsimps @{thm angle_def} :: @{thms Psi_defs}) [] [] 1\<close>)
(* reduce \<turnstile> \<box>A \<longrightarrow> \<diamond>Enabled B to \<turnstile> A \<longrightarrow> 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 @@
"\<turnstile> \<box>[(N1 \<or> N2) \<and> \<not>beta1]_(x,y,sem,pc1,pc2) \<and> SF(N2)_(x,y,sem,pc1,pc2) \<and> \<box>#True
\<longrightarrow> (pc2 = #g \<leadsto> pc2 = #a)"
apply (rule SF1)
- apply (tactic \<open>action_simp_tac (@{context} addsimps @{thms Psi_defs}) [] [@{thm squareE}] 1\<close>)
- apply (tactic \<open>action_simp_tac (@{context} addsimps @{thm angle_def} :: @{thms Psi_defs})
+ apply (tactic \<open>action_simp_tac (\<^context> addsimps @{thms Psi_defs}) [] [@{thm squareE}] 1\<close>)
+ apply (tactic \<open>action_simp_tac (\<^context> addsimps @{thm angle_def} :: @{thms Psi_defs})
[] [] 1\<close>)
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 @@
\<longrightarrow> (pc2 = #b \<leadsto> pc2 = #g)"
apply (rule SF1)
apply (tactic
- \<open>action_simp_tac (@{context} addsimps @{thms Psi_defs}) [] [@{thm squareE}] 1\<close>)
+ \<open>action_simp_tac (\<^context> addsimps @{thms Psi_defs}) [] [@{thm squareE}] 1\<close>)
apply (tactic
- \<open>action_simp_tac (@{context} addsimps @{thm angle_def} :: @{thms Psi_defs}) [] [] 1\<close>)
+ \<open>action_simp_tac (\<^context> addsimps @{thm angle_def} :: @{thms Psi_defs}) [] [] 1\<close>)
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 @@
\<and> SF(N1)_(x,y,sem,pc1,pc2) \<and> \<box> SF(N2)_(x,y,sem,pc1,pc2)
\<longrightarrow> (pc1 = #a \<leadsto> pc1 = #b)"
apply (rule SF1)
- apply (tactic \<open>action_simp_tac (@{context} addsimps @{thms Psi_defs}) [] [@{thm squareE}] 1\<close>)
+ apply (tactic \<open>action_simp_tac (\<^context> addsimps @{thms Psi_defs}) [] [@{thm squareE}] 1\<close>)
apply (tactic
- \<open>action_simp_tac (@{context} addsimps (@{thm angle_def} :: @{thms Psi_defs})) [] [] 1\<close>)
+ \<open>action_simp_tac (\<^context> addsimps (@{thm angle_def} :: @{thms Psi_defs})) [] [] 1\<close>)
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)