# HG changeset patch
# User wenzelm
# Date 1435337479 -7200
# Node ID c9bd1d902f045121aea3bc420209320517343299
# Parent  e0b77517f9a9b2bdc032aad46c621640a20a9159
isabelle update_cartouches;

diff -r e0b77517f9a9 -r c9bd1d902f04 src/HOL/TLA/Action.thy
--- a/src/HOL/TLA/Action.thy	Fri Jun 26 15:55:44 2015 +0200
+++ b/src/HOL/TLA/Action.thy	Fri Jun 26 18:51:19 2015 +0200
@@ -3,7 +3,7 @@
     Copyright:  1998 University of Munich
 *)
 
-section {* The action level of TLA as an Isabelle theory *}
+section \<open>The action level of TLA as an Isabelle theory\<close>
 
 theory Action
 imports Stfun
@@ -102,7 +102,7 @@
 
 (* ================ Functions to "unlift" action theorems into HOL rules ================ *)
 
-ML {*
+ML \<open>
 (* The following functions are specialized versions of the corresponding
    functions defined in Intensional.ML in that they introduce a
    "world" parameter of the form (s,t) and apply additional rewrites.
@@ -120,14 +120,14 @@
       Const _ $ (Const (@{const_name Valid}, _) $ _) =>
               (flatten (action_unlift ctxt th) handle THM _ => th)
     | _ => th;
-*}
+\<close>
 
 attribute_setup action_unlift =
-  {* Scan.succeed (Thm.rule_attribute (action_unlift o Context.proof_of)) *}
+  \<open>Scan.succeed (Thm.rule_attribute (action_unlift o Context.proof_of))\<close>
 attribute_setup action_rewrite =
-  {* Scan.succeed (Thm.rule_attribute (action_rewrite o Context.proof_of)) *}
+  \<open>Scan.succeed (Thm.rule_attribute (action_rewrite o Context.proof_of))\<close>
 attribute_setup action_use =
-  {* Scan.succeed (Thm.rule_attribute (action_use o Context.proof_of)) *}
+  \<open>Scan.succeed (Thm.rule_attribute (action_use o Context.proof_of))\<close>
 
 
 (* =========================== square / angle brackets =========================== *)
@@ -256,7 +256,7 @@
 
 (* ======================= action_simp_tac ============================== *)
 
-ML {*
+ML \<open>
 (* A dumb simplification-based tactic with just a little first-order logic:
    should plug in only "very safe" rules that can be applied blindly.
    Note that it applies whatever simplifications are currently active.
@@ -267,11 +267,11 @@
                                     @ [refl,impI,conjI,@{thm actionI},@{thm intI},allI]))
                       ORELSE' (eresolve_tac ctxt ((map (action_use ctxt) elims)
                                              @ [conjE,disjE,exE]))));
-*}
+\<close>
 
 (* ---------------- enabled_tac: tactic to prove (Enabled A) -------------------- *)
 
-ML {*
+ML \<open>
 (* "Enabled A" can be proven as follows:
    - Assume that we know which state variables are "base variables"
      this should be expressed by a theorem of the form "basevars (x,y,z,...)".
@@ -284,11 +284,11 @@
 
 fun enabled_tac ctxt base_vars =
   clarsimp_tac (ctxt addSIs [base_vars RS @{thm base_enabled}]);
-*}
+\<close>
 
-method_setup enabled = {*
+method_setup enabled = \<open>
   Attrib.thm >> (fn th => fn ctxt => SIMPLE_METHOD' (enabled_tac ctxt th))
-*}
+\<close>
 
 (* Example *)
 
diff -r e0b77517f9a9 -r c9bd1d902f04 src/HOL/TLA/Buffer/Buffer.thy
--- a/src/HOL/TLA/Buffer/Buffer.thy	Fri Jun 26 15:55:44 2015 +0200
+++ b/src/HOL/TLA/Buffer/Buffer.thy	Fri Jun 26 18:51:19 2015 +0200
@@ -2,7 +2,7 @@
     Author:     Stephan Merz, University of Munich
 *)
 
-section {* A simple FIFO buffer (synchronous communication, interleaving) *}
+section \<open>A simple FIFO buffer (synchronous communication, interleaving)\<close>
 
 theory Buffer
 imports "../TLA"
diff -r e0b77517f9a9 -r c9bd1d902f04 src/HOL/TLA/Buffer/DBuffer.thy
--- a/src/HOL/TLA/Buffer/DBuffer.thy	Fri Jun 26 15:55:44 2015 +0200
+++ b/src/HOL/TLA/Buffer/DBuffer.thy	Fri Jun 26 18:51:19 2015 +0200
@@ -2,7 +2,7 @@
     Author:     Stephan Merz, University of Munich
 *)
 
-section {* Two FIFO buffers in a row, with interleaving assumption *}
+section \<open>Two FIFO buffers in a row, with interleaving assumption\<close>
 
 theory DBuffer
 imports Buffer
@@ -59,7 +59,7 @@
   apply (rule square_simulation)
    apply clarsimp
   apply (tactic
-    {* action_simp_tac (@{context} addsimps (@{thm hd_append} :: @{thms db_defs})) [] [] 1 *})
+    \<open>action_simp_tac (@{context} addsimps (@{thm hd_append} :: @{thms db_defs})) [] [] 1\<close>)
   done
 
 
diff -r e0b77517f9a9 -r c9bd1d902f04 src/HOL/TLA/Inc/Inc.thy
--- a/src/HOL/TLA/Inc/Inc.thy	Fri Jun 26 15:55:44 2015 +0200
+++ b/src/HOL/TLA/Inc/Inc.thy	Fri Jun 26 18:51:19 2015 +0200
@@ -2,7 +2,7 @@
     Author:     Stephan Merz, University of Munich
 *)
 
-section {* Lamport's "increment" example *}
+section \<open>Lamport's "increment" example\<close>
 
 theory Inc
 imports "../TLA"
@@ -170,9 +170,9 @@
     \<longrightarrow> (pc1 = #g \<leadsto> pc1 = #a)"
   apply (rule SF1)
     apply (tactic
-      {* action_simp_tac (@{context} addsimps @{thms Psi_defs}) [] [@{thm squareE}] 1 *})
+      \<open>action_simp_tac (@{context} addsimps @{thms Psi_defs}) [] [@{thm squareE}] 1\<close>)
    apply (tactic
-      {* action_simp_tac (@{context} addsimps @{thm angle_def} :: @{thms Psi_defs}) [] [] 1 *})
+      \<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,9 +191,9 @@
   "\<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 {* 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 (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)
   done
@@ -211,9 +211,9 @@
     \<longrightarrow> (pc2 = #b \<leadsto> pc2 = #g)"
   apply (rule SF1)
     apply (tactic
-      {* action_simp_tac (@{context} addsimps @{thms Psi_defs}) [] [@{thm squareE}] 1 *})
+      \<open>action_simp_tac (@{context} addsimps @{thms Psi_defs}) [] [@{thm squareE}] 1\<close>)
    apply (tactic
-     {* action_simp_tac (@{context} addsimps @{thm angle_def} :: @{thms Psi_defs}) [] [] 1 *})
+     \<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 {* action_simp_tac (@{context} addsimps @{thms Psi_defs}) [] [@{thm squareE}] 1 *})
+  apply (tactic \<open>action_simp_tac (@{context} addsimps @{thms Psi_defs}) [] [@{thm squareE}] 1\<close>)
   apply (tactic
-    {* action_simp_tac (@{context} addsimps (@{thm angle_def} :: @{thms Psi_defs})) [] [] 1 *})
+    \<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)
diff -r e0b77517f9a9 -r c9bd1d902f04 src/HOL/TLA/Intensional.thy
--- a/src/HOL/TLA/Intensional.thy	Fri Jun 26 15:55:44 2015 +0200
+++ b/src/HOL/TLA/Intensional.thy	Fri Jun 26 18:51:19 2015 +0200
@@ -3,8 +3,8 @@
     Copyright:  1998 University of Munich
 *)
 
-section {* A framework for "intensional" (possible-world based) logics
-  on top of HOL, with lifting of constants and functions *}
+section \<open>A framework for "intensional" (possible-world based) logics
+  on top of HOL, with lifting of constants and functions\<close>
 
 theory Intensional
 imports Main
@@ -147,7 +147,7 @@
   unl_Rex1:    "w \<Turnstile> \<exists>!x. A x  ==  \<exists>!x. (w \<Turnstile> A x)"
 
 
-subsection {* Lemmas and tactics for "intensional" logics. *}
+subsection \<open>Lemmas and tactics for "intensional" logics.\<close>
 
 lemmas intensional_rews [simp] =
   unl_con unl_lift unl_lift2 unl_lift3 unl_Rall unl_Rex unl_Rex1
@@ -203,7 +203,7 @@
 
 (* ======== Functions to "unlift" intensional implications into HOL rules ====== *)
 
-ML {*
+ML \<open>
 (* Basic unlifting introduces a parameter "w" and applies basic rewrites, e.g.
    \<turnstile> F = G    becomes   F w = G w
    \<turnstile> F \<longrightarrow> G  becomes   F w \<longrightarrow> G w
@@ -253,15 +253,15 @@
       Const _ $ (Const (@{const_name Valid}, _) $ _) =>
               (flatten (int_unlift ctxt th) handle THM _ => th)
     | _ => th
-*}
+\<close>
 
 attribute_setup int_unlift =
-  {* Scan.succeed (Thm.rule_attribute (int_unlift o Context.proof_of)) *}
+  \<open>Scan.succeed (Thm.rule_attribute (int_unlift o Context.proof_of))\<close>
 attribute_setup int_rewrite =
-  {* Scan.succeed (Thm.rule_attribute (int_rewrite o Context.proof_of)) *}
-attribute_setup flatten = {* Scan.succeed (Thm.rule_attribute (K flatten)) *}
+  \<open>Scan.succeed (Thm.rule_attribute (int_rewrite o Context.proof_of))\<close>
+attribute_setup flatten = \<open>Scan.succeed (Thm.rule_attribute (K flatten))\<close>
 attribute_setup int_use =
-  {* Scan.succeed (Thm.rule_attribute (int_use o Context.proof_of)) *}
+  \<open>Scan.succeed (Thm.rule_attribute (int_use o Context.proof_of))\<close>
 
 lemma Not_Rall: "\<turnstile> (\<not>(\<forall>x. F x)) = (\<exists>x. \<not>F x)"
   by (simp add: Valid_def)
diff -r e0b77517f9a9 -r c9bd1d902f04 src/HOL/TLA/Memory/MemClerk.thy
--- a/src/HOL/TLA/Memory/MemClerk.thy	Fri Jun 26 15:55:44 2015 +0200
+++ b/src/HOL/TLA/Memory/MemClerk.thy	Fri Jun 26 18:51:19 2015 +0200
@@ -2,7 +2,7 @@
     Author:     Stephan Merz, University of Munich
 *)
 
-section {* RPC-Memory example: specification of the memory clerk *}
+section \<open>RPC-Memory example: specification of the memory clerk\<close>
 
 theory MemClerk
 imports Memory RPC MemClerkParameters
@@ -85,9 +85,9 @@
 lemma MClkFwd_enabled: "\<And>p. basevars (rtrner send!p, caller rcv!p, cst!p) \<Longrightarrow>  
       \<turnstile> Calling send p \<and> \<not>Calling rcv p \<and> cst!p = #clkA   
          \<longrightarrow> Enabled (MClkFwd send rcv cst p)"
-  by (tactic {* action_simp_tac (@{context} addsimps [@{thm MClkFwd_def},
+  by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm MClkFwd_def},
     @{thm Call_def}, @{thm caller_def}, @{thm rtrner_def}]) [exI]
-    [@{thm base_enabled}, @{thm Pair_inject}] 1 *})
+    [@{thm base_enabled}, @{thm Pair_inject}] 1\<close>)
 
 lemma MClkFwd_ch_enabled: "\<turnstile> Enabled (MClkFwd send rcv cst p)  \<longrightarrow>   
          Enabled (<MClkFwd send rcv cst p>_(cst!p, rtrner send!p, caller rcv!p))"
@@ -100,11 +100,11 @@
 lemma MClkReply_enabled: "\<And>p. basevars (rtrner send!p, caller rcv!p, cst!p) \<Longrightarrow>  
       \<turnstile> Calling send p \<and> \<not>Calling rcv p \<and> cst!p = #clkB   
          \<longrightarrow> Enabled (<MClkReply send rcv cst p>_(cst!p, rtrner send!p, caller rcv!p))"
-  apply (tactic {* action_simp_tac @{context}
-    [@{thm MClkReply_change} RSN (2, @{thm enabled_mono})] [] 1 *})
-  apply (tactic {* action_simp_tac (@{context} addsimps
+  apply (tactic \<open>action_simp_tac @{context}
+    [@{thm MClkReply_change} RSN (2, @{thm enabled_mono})] [] 1\<close>)
+  apply (tactic \<open>action_simp_tac (@{context} addsimps
     [@{thm MClkReply_def}, @{thm Return_def}, @{thm caller_def}, @{thm rtrner_def}])
-    [exI] [@{thm base_enabled}, @{thm Pair_inject}] 1 *})
+    [exI] [@{thm base_enabled}, @{thm Pair_inject}] 1\<close>)
   done
 
 lemma MClkReplyNotRetry: "\<turnstile> MClkReply send rcv cst p \<longrightarrow> \<not>MClkRetry send rcv cst p"
diff -r e0b77517f9a9 -r c9bd1d902f04 src/HOL/TLA/Memory/MemClerkParameters.thy
--- a/src/HOL/TLA/Memory/MemClerkParameters.thy	Fri Jun 26 15:55:44 2015 +0200
+++ b/src/HOL/TLA/Memory/MemClerkParameters.thy	Fri Jun 26 18:51:19 2015 +0200
@@ -2,7 +2,7 @@
     Author:     Stephan Merz, University of Munich
 *)
 
-section {* RPC-Memory example: Parameters of the memory clerk *}
+section \<open>RPC-Memory example: Parameters of the memory clerk\<close>
 
 theory MemClerkParameters
 imports RPCParameters
diff -r e0b77517f9a9 -r c9bd1d902f04 src/HOL/TLA/Memory/Memory.thy
--- a/src/HOL/TLA/Memory/Memory.thy	Fri Jun 26 15:55:44 2015 +0200
+++ b/src/HOL/TLA/Memory/Memory.thy	Fri Jun 26 18:51:19 2015 +0200
@@ -2,7 +2,7 @@
     Author:     Stephan Merz, University of Munich
 *)
 
-section {* RPC-Memory example: Memory specification *}
+section \<open>RPC-Memory example: Memory specification\<close>
 
 theory Memory
 imports MemoryParameters ProcedureInterface
@@ -176,10 +176,10 @@
       \<turnstile> Calling ch p \<and> (rs!p \<noteq> #NotAResult)
          \<longrightarrow> Enabled (<MemReturn ch rs p>_(rtrner ch ! p, rs!p))"
   apply (tactic
-    {* action_simp_tac @{context} [@{thm MemReturn_change} RSN (2, @{thm enabled_mono}) ] [] 1 *})
+    \<open>action_simp_tac @{context} [@{thm MemReturn_change} RSN (2, @{thm enabled_mono}) ] [] 1\<close>)
   apply (tactic
-    {* action_simp_tac (@{context} addsimps [@{thm MemReturn_def}, @{thm Return_def},
-      @{thm rtrner_def}]) [exI] [@{thm base_enabled}, @{thm Pair_inject}] 1 *})
+    \<open>action_simp_tac (@{context} addsimps [@{thm MemReturn_def}, @{thm Return_def},
+      @{thm rtrner_def}]) [exI] [@{thm base_enabled}, @{thm Pair_inject}] 1\<close>)
   done
 
 lemma ReadInner_enabled: "\<And>p. basevars (rtrner ch ! p, rs!p) \<Longrightarrow>
@@ -222,13 +222,13 @@
          \<longrightarrow> Enabled (<RNext ch mm rs p>_(rtrner ch ! p, rs!p))"
   apply (auto simp: enabled_disj [try_rewrite] intro!: RWRNext_enabled [temp_use])
   apply (case_tac "arg (ch w p)")
-   apply (tactic {* action_simp_tac (@{context} addsimps [@{thm Read_def},
-     temp_rewrite @{context} @{thm enabled_ex}]) [@{thm ReadInner_enabled}, exI] [] 1 *})
+   apply (tactic \<open>action_simp_tac (@{context} addsimps [@{thm Read_def},
+     temp_rewrite @{context} @{thm enabled_ex}]) [@{thm ReadInner_enabled}, exI] [] 1\<close>)
    apply (force dest: base_pair [temp_use])
   apply (erule contrapos_np)
-  apply (tactic {* action_simp_tac (@{context} addsimps [@{thm Write_def},
+  apply (tactic \<open>action_simp_tac (@{context} addsimps [@{thm Write_def},
     temp_rewrite @{context} @{thm enabled_ex}])
-    [@{thm WriteInner_enabled}, exI] [] 1 *})
+    [@{thm WriteInner_enabled}, exI] [] 1\<close>)
   done
 
 end
diff -r e0b77517f9a9 -r c9bd1d902f04 src/HOL/TLA/Memory/MemoryImplementation.thy
--- a/src/HOL/TLA/Memory/MemoryImplementation.thy	Fri Jun 26 15:55:44 2015 +0200
+++ b/src/HOL/TLA/Memory/MemoryImplementation.thy	Fri Jun 26 18:51:19 2015 +0200
@@ -2,7 +2,7 @@
     Author:     Stephan Merz, University of Munich
 *)
 
-section {* RPC-Memory example: Memory implementation *}
+section \<open>RPC-Memory example: Memory implementation\<close>
 
 theory MemoryImplementation
 imports Memory RPC MemClerk
@@ -223,17 +223,17 @@
    THIS IS UNSAFE, BECAUSE IT DOESN'T RECORD THE CHOICES!!
    (but it can be a lot faster than the default setup)
 *)
-ML {*
+ML \<open>
   val config_fast_solver = Attrib.setup_config_bool @{binding fast_solver} (K false);
   val fast_solver = mk_solver "fast_solver" (fn ctxt =>
     if Config.get ctxt config_fast_solver
     then assume_tac ctxt ORELSE' (etac notE)
     else K no_tac);
-*}
+\<close>
 
-setup {* map_theory_simpset (fn ctxt => ctxt addSSolver fast_solver) *}
+setup \<open>map_theory_simpset (fn ctxt => ctxt addSSolver fast_solver)\<close>
 
-ML {* val temp_elim = make_elim oo temp_use *}
+ML \<open>val temp_elim = make_elim oo temp_use\<close>
 
 
 
@@ -248,10 +248,10 @@
   apply (rule historyI)
       apply assumption+
   apply (rule MI_base)
-  apply (tactic {* action_simp_tac (@{context} addsimps [@{thm HInit_def}]) [] [] 1 *})
+  apply (tactic \<open>action_simp_tac (@{context} addsimps [@{thm HInit_def}]) [] [] 1\<close>)
    apply (erule fun_cong)
-  apply (tactic {* action_simp_tac (@{context} addsimps [@{thm HNext_def}])
-    [@{thm busy_squareI}] [] 1 *})
+  apply (tactic \<open>action_simp_tac (@{context} addsimps [@{thm HNext_def}])
+    [@{thm busy_squareI}] [] 1\<close>)
   apply (erule fun_cong)
   done
 
@@ -350,9 +350,9 @@
 
 lemma S1Hist: "\<turnstile> [HNext rmhist p]_(c p,r p,m p,rmhist!p) \<and> $(S1 rmhist p)
          \<longrightarrow> unchanged (rmhist!p)"
-  by (tactic {* action_simp_tac (@{context} addsimps [@{thm HNext_def}, @{thm S_def},
+  by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm HNext_def}, @{thm S_def},
     @{thm S1_def}, @{thm MemReturn_def}, @{thm RPCFail_def}, @{thm MClkReply_def},
-    @{thm Return_def}]) [] [temp_use @{context} @{thm squareE}] 1 *})
+    @{thm Return_def}]) [] [temp_use @{context} @{thm squareE}] 1\<close>)
 
 
 (* ------------------------------ State S2 ---------------------------------------- *)
@@ -366,9 +366,9 @@
 lemma S2Forward: "\<turnstile> $(S2 rmhist p) \<and> MClkFwd memCh crCh cst p
          \<and> unchanged (e p, r p, m p, rmhist!p)
          \<longrightarrow> (S3 rmhist p)$"
-  by (tactic {* action_simp_tac (@{context} addsimps [@{thm MClkFwd_def},
+  by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm MClkFwd_def},
     @{thm Call_def}, @{thm e_def}, @{thm r_def}, @{thm m_def}, @{thm caller_def},
-    @{thm rtrner_def}, @{thm S_def}, @{thm S2_def}, @{thm S3_def}, @{thm Calling_def}]) [] [] 1 *})
+    @{thm rtrner_def}, @{thm S_def}, @{thm S2_def}, @{thm S3_def}, @{thm Calling_def}]) [] [] 1\<close>)
 
 lemma S2RPCUnch: "\<turnstile> [RPCNext crCh rmCh rst p]_(r p) \<and> $(S2 rmhist p) \<longrightarrow> unchanged (r p)"
   by (auto simp: S_def S2_def dest!: RPCidle [temp_use])
@@ -403,19 +403,19 @@
 lemma S3Forward: "\<turnstile> RPCFwd crCh rmCh rst p \<and> HNext rmhist p \<and> $(S3 rmhist p)
          \<and> unchanged (e p, c p, m p)
          \<longrightarrow> (S4 rmhist p)$ \<and> unchanged (rmhist!p)"
-  by (tactic {* action_simp_tac (@{context} addsimps [@{thm RPCFwd_def},
+  by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm RPCFwd_def},
     @{thm HNext_def}, @{thm MemReturn_def}, @{thm RPCFail_def},
     @{thm MClkReply_def}, @{thm Return_def}, @{thm Call_def}, @{thm e_def},
     @{thm c_def}, @{thm m_def}, @{thm caller_def}, @{thm rtrner_def}, @{thm S_def},
-    @{thm S3_def}, @{thm S4_def}, @{thm Calling_def}]) [] [] 1 *})
+    @{thm S3_def}, @{thm S4_def}, @{thm Calling_def}]) [] [] 1\<close>)
 
 lemma S3Fail: "\<turnstile> RPCFail crCh rmCh rst p \<and> $(S3 rmhist p) \<and> HNext rmhist p
          \<and> unchanged (e p, c p, m p)
          \<longrightarrow> (S6 rmhist p)$"
-  by (tactic {* action_simp_tac (@{context} addsimps [@{thm HNext_def},
+  by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm HNext_def},
     @{thm RPCFail_def}, @{thm Return_def}, @{thm e_def}, @{thm c_def},
     @{thm m_def}, @{thm caller_def}, @{thm rtrner_def}, @{thm MVOKBARF_def},
-    @{thm S_def}, @{thm S3_def}, @{thm S6_def}, @{thm Calling_def}]) [] [] 1 *})
+    @{thm S_def}, @{thm S3_def}, @{thm S6_def}, @{thm Calling_def}]) [] [] 1\<close>)
 
 lemma S3MemUnch: "\<turnstile> [RNext rmCh mm ires p]_(m p) \<and> $(S3 rmhist p) \<longrightarrow> unchanged (m p)"
   by (auto simp: S_def S3_def dest!: Memoryidle [temp_use])
@@ -439,12 +439,12 @@
 lemma S4ReadInner: "\<turnstile> ReadInner rmCh mm ires p l \<and> $(S4 rmhist p) \<and> unchanged (e p, c p, r p)
          \<and> HNext rmhist p \<and> $(MemInv mm l)
          \<longrightarrow> (S4 rmhist p)$ \<and> unchanged (rmhist!p)"
-  by (tactic {* action_simp_tac (@{context} addsimps [@{thm ReadInner_def},
+  by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm ReadInner_def},
     @{thm GoodRead_def}, @{thm BadRead_def}, @{thm HNext_def}, @{thm MemReturn_def},
     @{thm RPCFail_def}, @{thm MClkReply_def}, @{thm Return_def}, @{thm e_def},
     @{thm c_def}, @{thm r_def}, @{thm rtrner_def}, @{thm caller_def},
     @{thm MVNROKBA_def}, @{thm S_def}, @{thm S4_def}, @{thm RdRequest_def},
-    @{thm Calling_def}, @{thm MemInv_def}]) [] [] 1 *})
+    @{thm Calling_def}, @{thm MemInv_def}]) [] [] 1\<close>)
 
 lemma S4Read: "\<turnstile> Read rmCh mm ires p \<and> $(S4 rmhist p) \<and> unchanged (e p, c p, r p)
          \<and> HNext rmhist p \<and> (\<forall>l. $MemInv mm l)
@@ -453,11 +453,11 @@
 
 lemma S4WriteInner: "\<turnstile> WriteInner rmCh mm ires p l v \<and> $(S4 rmhist p) \<and> unchanged (e p, c p, r p) \<and> HNext rmhist p
          \<longrightarrow> (S4 rmhist p)$ \<and> unchanged (rmhist!p)"
-  by (tactic {* action_simp_tac (@{context} addsimps [@{thm WriteInner_def},
+  by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm WriteInner_def},
     @{thm GoodWrite_def}, @{thm BadWrite_def}, @{thm HNext_def}, @{thm MemReturn_def},
     @{thm RPCFail_def}, @{thm MClkReply_def}, @{thm Return_def}, @{thm e_def},
     @{thm c_def}, @{thm r_def}, @{thm rtrner_def}, @{thm caller_def}, @{thm MVNROKBA_def},
-    @{thm S_def}, @{thm S4_def}, @{thm WrRequest_def}, @{thm Calling_def}]) [] [] 1 *})
+    @{thm S_def}, @{thm S4_def}, @{thm WrRequest_def}, @{thm Calling_def}]) [] [] 1\<close>)
 
 lemma S4Write: "\<turnstile> Write rmCh mm ires p l \<and> $(S4 rmhist p) \<and> unchanged (e p, c p, r p)
          \<and> (HNext rmhist p)
@@ -492,17 +492,17 @@
 
 lemma S5Reply: "\<turnstile> RPCReply crCh rmCh rst p \<and> $(S5 rmhist p) \<and> unchanged (e p, c p, m p,rmhist!p)
        \<longrightarrow> (S6 rmhist p)$"
-  by (tactic {* action_simp_tac (@{context} addsimps [@{thm RPCReply_def},
+  by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm RPCReply_def},
     @{thm Return_def}, @{thm e_def}, @{thm c_def}, @{thm m_def}, @{thm MVOKBA_def},
     @{thm MVOKBARF_def}, @{thm caller_def}, @{thm rtrner_def}, @{thm S_def},
-    @{thm S5_def}, @{thm S6_def}, @{thm Calling_def}]) [] [] 1 *})
+    @{thm S5_def}, @{thm S6_def}, @{thm Calling_def}]) [] [] 1\<close>)
 
 lemma S5Fail: "\<turnstile> RPCFail crCh rmCh rst p \<and> $(S5 rmhist p) \<and> unchanged (e p, c p, m p,rmhist!p)
          \<longrightarrow> (S6 rmhist p)$"
-  by (tactic {* action_simp_tac (@{context} addsimps [@{thm RPCFail_def},
+  by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm RPCFail_def},
     @{thm Return_def}, @{thm e_def}, @{thm c_def}, @{thm m_def},
     @{thm MVOKBARF_def}, @{thm caller_def}, @{thm rtrner_def},
-    @{thm S_def}, @{thm S5_def}, @{thm S6_def}, @{thm Calling_def}]) [] [] 1 *})
+    @{thm S_def}, @{thm S5_def}, @{thm S6_def}, @{thm Calling_def}]) [] [] 1\<close>)
 
 lemma S5MemUnch: "\<turnstile> [RNext rmCh mm ires p]_(m p) \<and> $(S5 rmhist p) \<longrightarrow> unchanged (m p)"
   by (auto simp: S_def S5_def dest!: Memoryidle [temp_use])
@@ -525,18 +525,18 @@
 lemma S6Retry: "\<turnstile> MClkRetry memCh crCh cst p \<and> HNext rmhist p \<and> $S6 rmhist p
          \<and> unchanged (e p,r p,m p)
          \<longrightarrow> (S3 rmhist p)$ \<and> unchanged (rmhist!p)"
-  by (tactic {* action_simp_tac (@{context} addsimps [@{thm HNext_def},
+  by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm HNext_def},
     @{thm MClkReply_def}, @{thm MClkRetry_def}, @{thm Call_def}, @{thm Return_def},
     @{thm e_def}, @{thm r_def}, @{thm m_def}, @{thm caller_def}, @{thm rtrner_def},
-    @{thm S_def}, @{thm S6_def}, @{thm S3_def}, @{thm Calling_def}]) [] [] 1 *})
+    @{thm S_def}, @{thm S6_def}, @{thm S3_def}, @{thm Calling_def}]) [] [] 1\<close>)
 
 lemma S6Reply: "\<turnstile> MClkReply memCh crCh cst p \<and> HNext rmhist p \<and> $S6 rmhist p
          \<and> unchanged (e p,r p,m p)
          \<longrightarrow> (S1 rmhist p)$"
-  by (tactic {* action_simp_tac (@{context} addsimps [@{thm HNext_def},
+  by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm HNext_def},
     @{thm MemReturn_def}, @{thm RPCFail_def}, @{thm Return_def}, @{thm MClkReply_def},
     @{thm e_def}, @{thm r_def}, @{thm m_def}, @{thm caller_def}, @{thm rtrner_def},
-    @{thm S_def}, @{thm S6_def}, @{thm S1_def}, @{thm Calling_def}]) [] [] 1 *})
+    @{thm S_def}, @{thm S6_def}, @{thm S1_def}, @{thm Calling_def}]) [] [] 1\<close>)
 
 lemma S6RPCUnch: "\<turnstile> [RPCNext crCh rmCh rst p]_(r p) \<and> $S6 rmhist p \<longrightarrow> unchanged (r p)"
   by (auto simp: S_def S6_def dest!: RPCidle [temp_use])
@@ -565,9 +565,9 @@
 lemma Step1_2_1: "\<turnstile> [HNext rmhist p]_(c p,r p,m p, rmhist!p) \<and> ImpNext p
          \<and> \<not>unchanged (e p, c p, r p, m p, rmhist!p)  \<and> $S1 rmhist p
          \<longrightarrow> (S2 rmhist p)$ \<and> ENext p \<and> unchanged (c p, r p, m p)"
-  apply (tactic {* action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) []
+  apply (tactic \<open>action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) []
       (map (temp_elim @{context})
-        [@{thm S1ClerkUnch}, @{thm S1RPCUnch}, @{thm S1MemUnch}, @{thm S1Hist}]) 1 *})
+        [@{thm S1ClerkUnch}, @{thm S1RPCUnch}, @{thm S1MemUnch}, @{thm S1Hist}]) 1\<close>)
    using [[fast_solver]]
    apply (auto elim!: squareE [temp_use] intro!: S1Env [temp_use])
   done
@@ -576,9 +576,9 @@
          \<and> \<not>unchanged (e p, c p, r p, m p, rmhist!p) \<and> $S2 rmhist p
          \<longrightarrow> (S3 rmhist p)$ \<and> MClkFwd memCh crCh cst p
              \<and> unchanged (e p, r p, m p, rmhist!p)"
-  apply (tactic {* action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) []
+  apply (tactic \<open>action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) []
     (map (temp_elim @{context})
-      [@{thm S2EnvUnch}, @{thm S2RPCUnch}, @{thm S2MemUnch}, @{thm S2Hist}]) 1 *})
+      [@{thm S2EnvUnch}, @{thm S2RPCUnch}, @{thm S2MemUnch}, @{thm S2Hist}]) 1\<close>)
    using [[fast_solver]]
    apply (auto elim!: squareE [temp_use] intro!: S2Clerk [temp_use] S2Forward [temp_use])
   done
@@ -587,11 +587,11 @@
          \<and> \<not>unchanged (e p, c p, r p, m p, rmhist!p) \<and> $S3 rmhist p
          \<longrightarrow> ((S4 rmhist p)$ \<and> RPCFwd crCh rmCh rst p \<and> unchanged (e p, c p, m p, rmhist!p))
              \<or> ((S6 rmhist p)$ \<and> RPCFail crCh rmCh rst p \<and> unchanged (e p, c p, m p))"
-  apply (tactic {* action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) []
-    (map (temp_elim @{context}) [@{thm S3EnvUnch}, @{thm S3ClerkUnch}, @{thm S3MemUnch}]) 1 *})
-  apply (tactic {* action_simp_tac @{context} []
+  apply (tactic \<open>action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) []
+    (map (temp_elim @{context}) [@{thm S3EnvUnch}, @{thm S3ClerkUnch}, @{thm S3MemUnch}]) 1\<close>)
+  apply (tactic \<open>action_simp_tac @{context} []
     (@{thm squareE} ::
-      map (temp_elim @{context}) [@{thm S3RPC}, @{thm S3Forward}, @{thm S3Fail}]) 1 *})
+      map (temp_elim @{context}) [@{thm S3RPC}, @{thm S3Forward}, @{thm S3Fail}]) 1\<close>)
    apply (auto dest!: S3Hist [temp_use])
   done
 
@@ -601,11 +601,11 @@
          \<longrightarrow> ((S4 rmhist p)$ \<and> Read rmCh mm ires p \<and> unchanged (e p, c p, r p, rmhist!p))
              \<or> ((S4 rmhist p)$ \<and> (\<exists>l. Write rmCh mm ires p l) \<and> unchanged (e p, c p, r p, rmhist!p))
              \<or> ((S5 rmhist p)$ \<and> MemReturn rmCh ires p \<and> unchanged (e p, c p, r p))"
-  apply (tactic {* action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) []
-    (map (temp_elim @{context}) [@{thm S4EnvUnch}, @{thm S4ClerkUnch}, @{thm S4RPCUnch}]) 1 *})
-  apply (tactic {* action_simp_tac (@{context} addsimps [@{thm RNext_def}]) []
+  apply (tactic \<open>action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) []
+    (map (temp_elim @{context}) [@{thm S4EnvUnch}, @{thm S4ClerkUnch}, @{thm S4RPCUnch}]) 1\<close>)
+  apply (tactic \<open>action_simp_tac (@{context} addsimps [@{thm RNext_def}]) []
     (@{thm squareE} ::
-      map (temp_elim @{context}) [@{thm S4Read}, @{thm S4Write}, @{thm S4Return}]) 1 *})
+      map (temp_elim @{context}) [@{thm S4Read}, @{thm S4Write}, @{thm S4Return}]) 1\<close>)
   apply (auto dest!: S4Hist [temp_use])
   done
 
@@ -613,9 +613,9 @@
               \<and> \<not>unchanged (e p, c p, r p, m p, rmhist!p) \<and> $S5 rmhist p
          \<longrightarrow> ((S6 rmhist p)$ \<and> RPCReply crCh rmCh rst p \<and> unchanged (e p, c p, m p))
              \<or> ((S6 rmhist p)$ \<and> RPCFail crCh rmCh rst p \<and> unchanged (e p, c p, m p))"
-  apply (tactic {* action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) []
-    (map (temp_elim @{context}) [@{thm S5EnvUnch}, @{thm S5ClerkUnch}, @{thm S5MemUnch}, @{thm S5Hist}]) 1 *})
-  apply (tactic {* action_simp_tac @{context} [] [@{thm squareE}, temp_elim @{context} @{thm S5RPC}] 1 *})
+  apply (tactic \<open>action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) []
+    (map (temp_elim @{context}) [@{thm S5EnvUnch}, @{thm S5ClerkUnch}, @{thm S5MemUnch}, @{thm S5Hist}]) 1\<close>)
+  apply (tactic \<open>action_simp_tac @{context} [] [@{thm squareE}, temp_elim @{context} @{thm S5RPC}] 1\<close>)
    using [[fast_solver]]
    apply (auto elim!: squareE [temp_use] dest!: S5Reply [temp_use] S5Fail [temp_use])
   done
@@ -624,10 +624,10 @@
               \<and> \<not>unchanged (e p, c p, r p, m p, rmhist!p) \<and> $S6 rmhist p
          \<longrightarrow> ((S1 rmhist p)$ \<and> MClkReply memCh crCh cst p \<and> unchanged (e p, r p, m p))
              \<or> ((S3 rmhist p)$ \<and> MClkRetry memCh crCh cst p \<and> unchanged (e p,r p,m p,rmhist!p))"
-  apply (tactic {* action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) []
-    (map (temp_elim @{context}) [@{thm S6EnvUnch}, @{thm S6RPCUnch}, @{thm S6MemUnch}]) 1 *})
-  apply (tactic {* action_simp_tac @{context} []
-    (@{thm squareE} :: map (temp_elim @{context}) [@{thm S6Clerk}, @{thm S6Retry}, @{thm S6Reply}]) 1 *})
+  apply (tactic \<open>action_simp_tac (@{context} addsimps [@{thm ImpNext_def}]) []
+    (map (temp_elim @{context}) [@{thm S6EnvUnch}, @{thm S6RPCUnch}, @{thm S6MemUnch}]) 1\<close>)
+  apply (tactic \<open>action_simp_tac @{context} []
+    (@{thm squareE} :: map (temp_elim @{context}) [@{thm S6Clerk}, @{thm S6Retry}, @{thm S6Reply}]) 1\<close>)
      apply (auto dest: S6Hist [temp_use])
   done
 
@@ -638,8 +638,8 @@
 section "Initialization (Step 1.3)"
 
 lemma Step1_3: "\<turnstile> S1 rmhist p \<longrightarrow> PInit (resbar rmhist) p"
-  by (tactic {* action_simp_tac (@{context} addsimps [@{thm resbar_def},
-    @{thm PInit_def}, @{thm S_def}, @{thm S1_def}]) [] [] 1 *})
+  by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm resbar_def},
+    @{thm PInit_def}, @{thm S_def}, @{thm S1_def}]) [] [] 1\<close>)
 
 (* ----------------------------------------------------------------------
    Step 1.4: Implementation's next-state relation simulates specification's
@@ -656,17 +656,17 @@
 lemma Step1_4_2: "\<turnstile> MClkFwd memCh crCh cst p \<and> $S2 rmhist p \<and> (S3 rmhist p)$
          \<and> unchanged (e p, r p, m p, rmhist!p)
          \<longrightarrow> unchanged (rtrner memCh!p, resbar rmhist!p)"
-  by (tactic {* action_simp_tac
+  by (tactic \<open>action_simp_tac
     (@{context} addsimps [@{thm MClkFwd_def}, @{thm e_def}, @{thm r_def}, @{thm m_def},
-    @{thm resbar_def}, @{thm S_def}, @{thm S2_def}, @{thm S3_def}]) [] [] 1 *})
+    @{thm resbar_def}, @{thm S_def}, @{thm S2_def}, @{thm S3_def}]) [] [] 1\<close>)
 
 lemma Step1_4_3a: "\<turnstile> RPCFwd crCh rmCh rst p \<and> $S3 rmhist p \<and> (S4 rmhist p)$
          \<and> unchanged (e p, c p, m p, rmhist!p)
          \<longrightarrow> unchanged (rtrner memCh!p, resbar rmhist!p)"
   apply clarsimp
   apply (drule S3_excl [temp_use] S4_excl [temp_use])+
-  apply (tactic {* action_simp_tac (@{context} addsimps [@{thm e_def},
-    @{thm c_def}, @{thm m_def}, @{thm resbar_def}, @{thm S_def}, @{thm S3_def}]) [] [] 1 *})
+  apply (tactic \<open>action_simp_tac (@{context} addsimps [@{thm e_def},
+    @{thm c_def}, @{thm m_def}, @{thm resbar_def}, @{thm S_def}, @{thm S3_def}]) [] [] 1\<close>)
   done
 
 lemma Step1_4_3b: "\<turnstile> RPCFail crCh rmCh rst p \<and> $S3 rmhist p \<and> (S6 rmhist p)$
@@ -684,13 +684,13 @@
          \<longrightarrow> ReadInner memCh mm (resbar rmhist) p l"
   apply clarsimp
   apply (drule S4_excl [temp_use])+
-  apply (tactic {* action_simp_tac (@{context} addsimps [@{thm ReadInner_def},
-    @{thm GoodRead_def}, @{thm BadRead_def}, @{thm e_def}, @{thm c_def}, @{thm m_def}]) [] [] 1 *})
+  apply (tactic \<open>action_simp_tac (@{context} addsimps [@{thm ReadInner_def},
+    @{thm GoodRead_def}, @{thm BadRead_def}, @{thm e_def}, @{thm c_def}, @{thm m_def}]) [] [] 1\<close>)
      apply (auto simp: resbar_def)
-       apply (tactic {* ALLGOALS (action_simp_tac
+       apply (tactic \<open>ALLGOALS (action_simp_tac
                 (@{context} addsimps [@{thm RPCRelayArg_def}, @{thm MClkRelayArg_def},
                   @{thm S_def}, @{thm S4_def}, @{thm RdRequest_def}, @{thm MemInv_def}])
-                [] [@{thm impE}, @{thm MemValNotAResultE}]) *})
+                [] [@{thm impE}, @{thm MemValNotAResultE}])\<close>)
   done
 
 lemma Step1_4_4a: "\<turnstile> Read rmCh mm ires p \<and> $S4 rmhist p \<and> (S4 rmhist p)$
@@ -703,13 +703,13 @@
          \<longrightarrow> WriteInner memCh mm (resbar rmhist) p l v"
   apply clarsimp
   apply (drule S4_excl [temp_use])+
-  apply (tactic {* action_simp_tac (@{context} addsimps
+  apply (tactic \<open>action_simp_tac (@{context} addsimps
     [@{thm WriteInner_def}, @{thm GoodWrite_def}, @{thm BadWrite_def}, @{thm e_def},
-    @{thm c_def}, @{thm m_def}]) [] [] 1 *})
+    @{thm c_def}, @{thm m_def}]) [] [] 1\<close>)
      apply (auto simp: resbar_def)
-    apply (tactic {* ALLGOALS (action_simp_tac (@{context} addsimps
+    apply (tactic \<open>ALLGOALS (action_simp_tac (@{context} addsimps
       [@{thm RPCRelayArg_def}, @{thm MClkRelayArg_def}, @{thm S_def},
-      @{thm S4_def}, @{thm WrRequest_def}]) [] []) *})
+      @{thm S4_def}, @{thm WrRequest_def}]) [] [])\<close>)
   done
 
 lemma Step1_4_4b: "\<turnstile> Write rmCh mm ires p l \<and> $S4 rmhist p \<and> (S4 rmhist p)$
@@ -720,8 +720,8 @@
 lemma Step1_4_4c: "\<turnstile> MemReturn rmCh ires p \<and> $S4 rmhist p \<and> (S5 rmhist p)$
          \<and> unchanged (e p, c p, r p)
          \<longrightarrow> unchanged (rtrner memCh!p, resbar rmhist!p)"
-  apply (tactic {* action_simp_tac (@{context} addsimps [@{thm e_def},
-    @{thm c_def}, @{thm r_def}, @{thm resbar_def}]) [] [] 1 *})
+  apply (tactic \<open>action_simp_tac (@{context} addsimps [@{thm e_def},
+    @{thm c_def}, @{thm r_def}, @{thm resbar_def}]) [] [] 1\<close>)
   apply (drule S4_excl [temp_use] S5_excl [temp_use])+
   using [[fast_solver]]
   apply (auto elim!: squareE [temp_use] simp: MemReturn_def Return_def)
@@ -750,12 +750,12 @@
          \<longrightarrow> MemReturn memCh (resbar rmhist) p"
   apply clarsimp
   apply (drule S6_excl [temp_use])+
-  apply (tactic {* action_simp_tac (@{context} addsimps [@{thm e_def},
+  apply (tactic \<open>action_simp_tac (@{context} addsimps [@{thm e_def},
     @{thm r_def}, @{thm m_def}, @{thm MClkReply_def}, @{thm MemReturn_def},
-    @{thm Return_def}, @{thm resbar_def}]) [] [] 1 *})
+    @{thm Return_def}, @{thm resbar_def}]) [] [] 1\<close>)
     apply simp_all (* simplify if-then-else *)
-    apply (tactic {* ALLGOALS (action_simp_tac (@{context} addsimps
-      [@{thm MClkReplyVal_def}, @{thm S6_def}, @{thm S_def}]) [] [@{thm MVOKBARFnotNR}]) *})
+    apply (tactic \<open>ALLGOALS (action_simp_tac (@{context} addsimps
+      [@{thm MClkReplyVal_def}, @{thm S6_def}, @{thm S_def}]) [] [@{thm MVOKBARFnotNR}])\<close>)
   done
 
 lemma Step1_4_6b: "\<turnstile> MClkRetry memCh crCh cst p \<and> $S6 rmhist p \<and> (S3 rmhist p)$
@@ -763,8 +763,8 @@
          \<longrightarrow> MemFail memCh (resbar rmhist) p"
   apply clarsimp
   apply (drule S3_excl [temp_use])+
-  apply (tactic {* action_simp_tac (@{context} addsimps [@{thm e_def}, @{thm r_def},
-    @{thm m_def}, @{thm MClkRetry_def}, @{thm MemFail_def}, @{thm resbar_def}]) [] [] 1 *})
+  apply (tactic \<open>action_simp_tac (@{context} addsimps [@{thm e_def}, @{thm r_def},
+    @{thm m_def}, @{thm MClkRetry_def}, @{thm MemFail_def}, @{thm resbar_def}]) [] [] 1\<close>)
    apply (auto simp: S6_def S_def)
   done
 
@@ -794,7 +794,7 @@
 (* Frequently needed abbreviation: distinguish between idling and non-idling
    steps of the implementation, and try to solve the idling case by simplification
 *)
-ML {*
+ML \<open>
 fun split_idle_tac ctxt =
   SELECT_GOAL
    (TRY (rtac @{thm actionI} 1) THEN
@@ -802,12 +802,12 @@
     rewrite_goals_tac ctxt @{thms action_rews} THEN
     forward_tac ctxt [temp_use ctxt @{thm Step1_4_7}] 1 THEN
     asm_full_simp_tac ctxt 1);
-*}
+\<close>
 
-method_setup split_idle = {*
+method_setup split_idle = \<open>
   Method.sections (Simplifier.simp_modifiers @ Splitter.split_modifiers)
     >> (K (SIMPLE_METHOD' o split_idle_tac))
-*}
+\<close>
 
 (* ----------------------------------------------------------------------
    Combine steps 1.2 and 1.4 to prove that the implementation satisfies
@@ -901,15 +901,15 @@
 
 lemma S1_RNextdisabled: "\<turnstile> S1 rmhist p \<longrightarrow>
          \<not>Enabled (<RNext memCh mm (resbar rmhist) p>_(rtrner memCh!p, resbar rmhist!p))"
-  apply (tactic {* action_simp_tac (@{context} addsimps [@{thm angle_def},
-    @{thm S_def}, @{thm S1_def}]) [notI] [@{thm enabledE}, temp_elim @{context} @{thm Memoryidle}] 1 *})
+  apply (tactic \<open>action_simp_tac (@{context} addsimps [@{thm angle_def},
+    @{thm S_def}, @{thm S1_def}]) [notI] [@{thm enabledE}, temp_elim @{context} @{thm Memoryidle}] 1\<close>)
   apply force
   done
 
 lemma S1_Returndisabled: "\<turnstile> S1 rmhist p \<longrightarrow>
          \<not>Enabled (<MemReturn memCh (resbar rmhist) p>_(rtrner memCh!p, resbar rmhist!p))"
-  by (tactic {* action_simp_tac (@{context} addsimps [@{thm angle_def}, @{thm MemReturn_def},
-    @{thm Return_def}, @{thm S_def}, @{thm S1_def}]) [notI] [@{thm enabledE}] 1 *})
+  by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm angle_def}, @{thm MemReturn_def},
+    @{thm Return_def}, @{thm S_def}, @{thm S1_def}]) [notI] [@{thm enabledE}] 1\<close>)
 
 lemma RNext_fair: "\<turnstile> \<box>\<diamond>S1 rmhist p
          \<longrightarrow> WF(RNext memCh mm (resbar rmhist) p)_(rtrner memCh!p, resbar rmhist!p)"
@@ -1087,16 +1087,16 @@
 
 lemma MClkReplyS6:
   "\<turnstile> $ImpInv rmhist p \<and> <MClkReply memCh crCh cst p>_(c p) \<longrightarrow> $S6 rmhist p"
-  by (tactic {* action_simp_tac (@{context} addsimps [@{thm angle_def},
+  by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm angle_def},
     @{thm MClkReply_def}, @{thm Return_def}, @{thm ImpInv_def}, @{thm S_def},
-    @{thm S1_def}, @{thm S2_def}, @{thm S3_def}, @{thm S4_def}, @{thm S5_def}]) [] [] 1 *})
+    @{thm S1_def}, @{thm S2_def}, @{thm S3_def}, @{thm S4_def}, @{thm S5_def}]) [] [] 1\<close>)
 
 lemma S6MClkReply_enabled: "\<turnstile> S6 rmhist p \<longrightarrow> Enabled (<MClkReply memCh crCh cst p>_(c p))"
   apply (auto simp: c_def intro!: MClkReply_enabled [temp_use])
      apply (cut_tac MI_base)
      apply (blast dest: base_pair)
-    apply (tactic {* ALLGOALS (action_simp_tac (@{context}
-      addsimps [@{thm S_def}, @{thm S6_def}]) [] []) *})
+    apply (tactic \<open>ALLGOALS (action_simp_tac (@{context}
+      addsimps [@{thm S_def}, @{thm S6_def}]) [] [])\<close>)
   done
 
 lemma S6_live: "\<turnstile> \<box>(ImpNext p \<and> [HNext rmhist p]_(c p,r p,m p, rmhist!p) \<and> $(ImpInv rmhist p))
@@ -1106,8 +1106,8 @@
   apply (subgoal_tac "sigma \<Turnstile> \<box>\<diamond> (<MClkReply memCh crCh cst p>_ (c p))")
    apply (erule InfiniteEnsures)
     apply assumption
-   apply (tactic {* action_simp_tac @{context} []
-     (map (temp_elim @{context}) [@{thm MClkReplyS6}, @{thm S6MClkReply_successors}]) 1 *})
+   apply (tactic \<open>action_simp_tac @{context} []
+     (map (temp_elim @{context}) [@{thm MClkReplyS6}, @{thm S6MClkReply_successors}]) 1\<close>)
   apply (auto simp: SF_def)
   apply (erule contrapos_np)
   apply (auto intro!: S6MClkReply_enabled [temp_use] elim!: STL4E [temp_use] DmdImplE [temp_use])
@@ -1193,8 +1193,8 @@
          sigma \<Turnstile> \<box>\<diamond>S6 rmhist p \<longrightarrow> \<box>\<diamond>S1 rmhist p \<rbrakk>
       \<Longrightarrow> sigma \<Turnstile> \<box>\<diamond>S1 rmhist p"
   apply (rule classical)
-  apply (tactic {* asm_lr_simp_tac (@{context} addsimps
-    [temp_use @{context} @{thm NotBox}, temp_rewrite @{context} @{thm NotDmd}]) 1 *})
+  apply (tactic \<open>asm_lr_simp_tac (@{context} addsimps
+    [temp_use @{context} @{thm NotBox}, temp_rewrite @{context} @{thm NotDmd}]) 1\<close>)
   apply (auto elim!: leadsto_infinite [temp_use] mp dest!: DBImplBD [temp_use])
   done
 
diff -r e0b77517f9a9 -r c9bd1d902f04 src/HOL/TLA/Memory/MemoryParameters.thy
--- a/src/HOL/TLA/Memory/MemoryParameters.thy	Fri Jun 26 15:55:44 2015 +0200
+++ b/src/HOL/TLA/Memory/MemoryParameters.thy	Fri Jun 26 18:51:19 2015 +0200
@@ -2,7 +2,7 @@
     Author:     Stephan Merz, University of Munich
 *)
 
-section {* RPC-Memory example: Memory parameters *}
+section \<open>RPC-Memory example: Memory parameters\<close>
 
 theory MemoryParameters
 imports RPCMemoryParams
diff -r e0b77517f9a9 -r c9bd1d902f04 src/HOL/TLA/Memory/ProcedureInterface.thy
--- a/src/HOL/TLA/Memory/ProcedureInterface.thy	Fri Jun 26 15:55:44 2015 +0200
+++ b/src/HOL/TLA/Memory/ProcedureInterface.thy	Fri Jun 26 18:51:19 2015 +0200
@@ -2,7 +2,7 @@
     Author:     Stephan Merz, University of Munich
 *)
 
-section {* Procedure interface for RPC-Memory components *}
+section \<open>Procedure interface for RPC-Memory components\<close>
 
 theory ProcedureInterface
 imports "../TLA" RPCMemoryParams
diff -r e0b77517f9a9 -r c9bd1d902f04 src/HOL/TLA/Memory/RPC.thy
--- a/src/HOL/TLA/Memory/RPC.thy	Fri Jun 26 15:55:44 2015 +0200
+++ b/src/HOL/TLA/Memory/RPC.thy	Fri Jun 26 18:51:19 2015 +0200
@@ -2,7 +2,7 @@
     Author:     Stephan Merz, University of Munich
 *)
 
-section {* RPC-Memory example: RPC specification *}
+section \<open>RPC-Memory example: RPC specification\<close>
 
 theory RPC
 imports RPCParameters ProcedureInterface Memory
@@ -99,15 +99,15 @@
 (* Enabledness of some actions *)
 lemma RPCFail_enabled: "\<And>p. basevars (rtrner send!p, caller rcv!p, rst!p) \<Longrightarrow>  
     \<turnstile> \<not>Calling rcv p \<and> Calling send p \<longrightarrow> Enabled (RPCFail send rcv rst p)"
-  by (tactic {* action_simp_tac (@{context} addsimps [@{thm RPCFail_def},
+  by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm RPCFail_def},
     @{thm Return_def}, @{thm caller_def}, @{thm rtrner_def}]) [exI]
-    [@{thm base_enabled}, @{thm Pair_inject}] 1 *})
+    [@{thm base_enabled}, @{thm Pair_inject}] 1\<close>)
 
 lemma RPCReply_enabled: "\<And>p. basevars (rtrner send!p, caller rcv!p, rst!p) \<Longrightarrow>  
       \<turnstile> \<not>Calling rcv p \<and> Calling send p \<and> rst!p = #rpcB  
          \<longrightarrow> Enabled (RPCReply send rcv rst p)"
-  by (tactic {* action_simp_tac (@{context} addsimps [@{thm RPCReply_def},
+  by (tactic \<open>action_simp_tac (@{context} addsimps [@{thm RPCReply_def},
     @{thm Return_def}, @{thm caller_def}, @{thm rtrner_def}]) [exI]
-    [@{thm base_enabled}, @{thm Pair_inject}] 1 *})
+    [@{thm base_enabled}, @{thm Pair_inject}] 1\<close>)
 
 end
diff -r e0b77517f9a9 -r c9bd1d902f04 src/HOL/TLA/Memory/RPCMemoryParams.thy
--- a/src/HOL/TLA/Memory/RPCMemoryParams.thy	Fri Jun 26 15:55:44 2015 +0200
+++ b/src/HOL/TLA/Memory/RPCMemoryParams.thy	Fri Jun 26 18:51:19 2015 +0200
@@ -2,7 +2,7 @@
     Author:     Stephan Merz, University of Munich
 *)
 
-section {* Basic declarations for the RPC-memory example *}
+section \<open>Basic declarations for the RPC-memory example\<close>
 
 theory RPCMemoryParams
 imports Main
diff -r e0b77517f9a9 -r c9bd1d902f04 src/HOL/TLA/Memory/RPCParameters.thy
--- a/src/HOL/TLA/Memory/RPCParameters.thy	Fri Jun 26 15:55:44 2015 +0200
+++ b/src/HOL/TLA/Memory/RPCParameters.thy	Fri Jun 26 18:51:19 2015 +0200
@@ -2,7 +2,7 @@
     Author:     Stephan Merz, University of Munich
 *)
 
-section {* RPC-Memory example: RPC parameters *}
+section \<open>RPC-Memory example: RPC parameters\<close>
 
 theory RPCParameters
 imports MemoryParameters
diff -r e0b77517f9a9 -r c9bd1d902f04 src/HOL/TLA/Stfun.thy
--- a/src/HOL/TLA/Stfun.thy	Fri Jun 26 15:55:44 2015 +0200
+++ b/src/HOL/TLA/Stfun.thy	Fri Jun 26 18:51:19 2015 +0200
@@ -3,7 +3,7 @@
     Copyright:  1998 University of Munich
 *)
 
-section {* States and state functions for TLA as an "intensional" logic *}
+section \<open>States and state functions for TLA as an "intensional" logic\<close>
 
 theory Stfun
 imports Intensional
diff -r e0b77517f9a9 -r c9bd1d902f04 src/HOL/TLA/TLA.thy
--- a/src/HOL/TLA/TLA.thy	Fri Jun 26 15:55:44 2015 +0200
+++ b/src/HOL/TLA/TLA.thy	Fri Jun 26 18:51:19 2015 +0200
@@ -3,7 +3,7 @@
     Copyright:  1998 University of Munich
 *)
 
-section {* The temporal level of TLA *}
+section \<open>The temporal level of TLA\<close>
 
 theory TLA
 imports Init
@@ -102,7 +102,7 @@
 
 (* ======== Functions to "unlift" temporal theorems ====== *)
 
-ML {*
+ML \<open>
 (* The following functions are specialized versions of the corresponding
    functions defined in theory Intensional in that they introduce a
    "world" parameter of type "behavior".
@@ -121,16 +121,16 @@
   | _ => th;
 
 fun try_rewrite ctxt th = temp_rewrite ctxt th handle THM _ => temp_use ctxt th;
-*}
+\<close>
 
 attribute_setup temp_unlift =
-  {* Scan.succeed (Thm.rule_attribute (temp_unlift o Context.proof_of)) *}
+  \<open>Scan.succeed (Thm.rule_attribute (temp_unlift o Context.proof_of))\<close>
 attribute_setup temp_rewrite =
-  {* Scan.succeed (Thm.rule_attribute (temp_rewrite o Context.proof_of)) *}
+  \<open>Scan.succeed (Thm.rule_attribute (temp_rewrite o Context.proof_of))\<close>
 attribute_setup temp_use =
-  {* Scan.succeed (Thm.rule_attribute (temp_use o Context.proof_of)) *}
+  \<open>Scan.succeed (Thm.rule_attribute (temp_use o Context.proof_of))\<close>
 attribute_setup try_rewrite =
-  {* Scan.succeed (Thm.rule_attribute (try_rewrite o Context.proof_of)) *}
+  \<open>Scan.succeed (Thm.rule_attribute (try_rewrite o Context.proof_of))\<close>
 
 
 (* ------------------------------------------------------------------------- *)
@@ -283,7 +283,7 @@
 
 lemma box_thin: "\<lbrakk> sigma \<Turnstile> \<box>F; PROP W \<rbrakk> \<Longrightarrow> PROP W" .
 
-ML {*
+ML \<open>
 fun merge_box_tac i =
    REPEAT_DETERM (EVERY [etac @{thm box_conjE} i, atac i, etac @{thm box_thin} i])
 
@@ -298,12 +298,12 @@
 fun merge_act_box_tac ctxt i =
   REPEAT_DETERM (EVERY [etac @{thm box_conjE_act} i, atac i,
     Rule_Insts.eres_inst_tac ctxt [((("'a", 0), Position.none), "state * state")] [] @{thm box_thin} i])
-*}
+\<close>
 
-method_setup merge_box = {* Scan.succeed (K (SIMPLE_METHOD' merge_box_tac)) *}
-method_setup merge_temp_box = {* Scan.succeed (SIMPLE_METHOD' o merge_temp_box_tac) *}
-method_setup merge_stp_box = {* Scan.succeed (SIMPLE_METHOD' o merge_stp_box_tac) *}
-method_setup merge_act_box = {* Scan.succeed (SIMPLE_METHOD' o merge_act_box_tac) *}
+method_setup merge_box = \<open>Scan.succeed (K (SIMPLE_METHOD' merge_box_tac))\<close>
+method_setup merge_temp_box = \<open>Scan.succeed (SIMPLE_METHOD' o merge_temp_box_tac)\<close>
+method_setup merge_stp_box = \<open>Scan.succeed (SIMPLE_METHOD' o merge_stp_box_tac)\<close>
+method_setup merge_act_box = \<open>Scan.succeed (SIMPLE_METHOD' o merge_act_box_tac)\<close>
 
 (* rewrite rule to push universal quantification through box:
       (sigma \<Turnstile> \<box>(\<forall>x. F x)) = (\<forall>x. (sigma \<Turnstile> \<box>F x))
@@ -571,7 +571,7 @@
 
 (* ---------------- (Semi-)automatic invariant tactics ---------------------- *)
 
-ML {*
+ML \<open>
 (* inv_tac reduces goals of the form ... \<Longrightarrow> sigma \<Turnstile> \<box>P *)
 fun inv_tac ctxt =
   SELECT_GOAL
@@ -592,15 +592,15 @@
     (inv_tac ctxt 1 THEN
       (TRYALL (action_simp_tac
         (ctxt addsimps [@{thm Init_stp}, @{thm Init_act}]) [] [@{thm squareE}])));
-*}
+\<close>
 
-method_setup invariant = {*
+method_setup invariant = \<open>
   Method.sections Clasimp.clasimp_modifiers >> (K (SIMPLE_METHOD' o inv_tac))
-*}
+\<close>
 
-method_setup auto_invariant = {*
+method_setup auto_invariant = \<open>
   Method.sections Clasimp.clasimp_modifiers >> (K (SIMPLE_METHOD' o auto_inv_tac))
-*}
+\<close>
 
 lemma unless: "\<turnstile> \<box>($P \<longrightarrow> P` \<or> Q`) \<longrightarrow> (stable P) \<or> \<diamond>Q"
   apply (unfold dmd_def)
@@ -685,10 +685,10 @@
   done
 
 (* A tactic that "boxes" all fairness conditions. Apply more_temp_simps to "unbox". *)
-ML {*
+ML \<open>
 fun box_fair_tac ctxt =
   SELECT_GOAL (REPEAT (dresolve_tac ctxt [@{thm BoxWFI}, @{thm BoxSFI}] 1))
-*}
+\<close>
 
 
 (* ------------------------------ leads-to ------------------------------ *)