# HG changeset patch
# User wenzelm
# Date 1451509072 -3600
# Node ID f1599e98c4d08c369303af5a68d5e4d5936a219f
# Parent  1f2788fb0b8beff0eefc177ac895b69733367a80
isabelle update_cartouches -c -t;

diff -r 1f2788fb0b8b -r f1599e98c4d0 src/HOL/HOLCF/IOA/ABP/Abschannel.thy
--- a/src/HOL/HOLCF/IOA/ABP/Abschannel.thy	Wed Dec 30 21:56:12 2015 +0100
+++ b/src/HOL/HOLCF/IOA/ABP/Abschannel.thy	Wed Dec 30 21:57:52 2015 +0100
@@ -2,7 +2,7 @@
     Author:     Olaf Müller
 *)
 
-section {* The transmission channel *}
+section \<open>The transmission channel\<close>
 
 theory Abschannel
 imports "~~/src/HOL/HOLCF/IOA/meta_theory/IOA" Action Lemmas
diff -r 1f2788fb0b8b -r f1599e98c4d0 src/HOL/HOLCF/IOA/ABP/Abschannel_finite.thy
--- a/src/HOL/HOLCF/IOA/ABP/Abschannel_finite.thy	Wed Dec 30 21:56:12 2015 +0100
+++ b/src/HOL/HOLCF/IOA/ABP/Abschannel_finite.thy	Wed Dec 30 21:57:52 2015 +0100
@@ -2,7 +2,7 @@
     Author:     Olaf Müller
 *)
 
-section {* The transmission channel -- finite version *}
+section \<open>The transmission channel -- finite version\<close>
 
 theory Abschannel_finite
 imports Abschannel "~~/src/HOL/HOLCF/IOA/meta_theory/IOA" Action Lemmas
diff -r 1f2788fb0b8b -r f1599e98c4d0 src/HOL/HOLCF/IOA/ABP/Action.thy
--- a/src/HOL/HOLCF/IOA/ABP/Action.thy	Wed Dec 30 21:56:12 2015 +0100
+++ b/src/HOL/HOLCF/IOA/ABP/Action.thy	Wed Dec 30 21:57:52 2015 +0100
@@ -2,7 +2,7 @@
     Author:     Olaf Müller
 *)
 
-section {* The set of all actions of the system *}
+section \<open>The set of all actions of the system\<close>
 
 theory Action
 imports Packet
diff -r 1f2788fb0b8b -r f1599e98c4d0 src/HOL/HOLCF/IOA/ABP/Correctness.thy
--- a/src/HOL/HOLCF/IOA/ABP/Correctness.thy	Wed Dec 30 21:56:12 2015 +0100
+++ b/src/HOL/HOLCF/IOA/ABP/Correctness.thy	Wed Dec 30 21:57:52 2015 +0100
@@ -2,7 +2,7 @@
     Author:     Olaf Müller
 *)
 
-section {* The main correctness proof: System_fin implements System *}
+section \<open>The main correctness proof: System_fin implements System\<close>
 
 theory Correctness
 imports "~~/src/HOL/HOLCF/IOA/meta_theory/IOA" Env Impl Impl_finite
@@ -67,7 +67,7 @@
   asig_projections set_lemmas
 
 
-subsection {* lemmas about reduce *}
+subsection \<open>lemmas about reduce\<close>
 
 lemma l_iff_red_nil: "(reduce l = []) = (l = [])"
   by (induct l) (auto split: list.split)
@@ -75,28 +75,28 @@
 lemma hd_is_reduce_hd: "s ~= [] --> hd s = hd (reduce s)"
   by (induct s) (auto split: list.split)
 
-text {* to be used in the following Lemma *}
+text \<open>to be used in the following Lemma\<close>
 lemma rev_red_not_nil [rule_format]:
     "l ~= [] --> reverse (reduce l) ~= []"
   by (induct l) (auto split: list.split)
 
-text {* shows applicability of the induction hypothesis of the following Lemma 1 *}
+text \<open>shows applicability of the induction hypothesis of the following Lemma 1\<close>
 lemma last_ind_on_first:
     "l ~= [] ==> hd (reverse (reduce (a # l))) = hd (reverse (reduce l))"
   apply simp
-  apply (tactic {* auto_tac (put_simpset HOL_ss @{context}
+  apply (tactic \<open>auto_tac (put_simpset HOL_ss @{context}
     addsimps (@{thms reverse.simps} @ [@{thm hd_append}, @{thm rev_red_not_nil}])
-    |> Splitter.add_split @{thm list.split}) *})
+    |> Splitter.add_split @{thm list.split})\<close>)
   done
 
-text {* Main Lemma 1 for @{text "S_pkt"} in showing that reduce is refinement. *}
+text \<open>Main Lemma 1 for \<open>S_pkt\<close> in showing that reduce is refinement.\<close>
 lemma reduce_hd:
    "if x=hd(reverse(reduce(l))) & reduce(l)~=[] then
        reduce(l@[x])=reduce(l) else
        reduce(l@[x])=reduce(l)@[x]"
 apply (simplesubst split_if)
 apply (rule conjI)
-txt {* @{text "-->"} *}
+txt \<open>\<open>-->\<close>\<close>
 apply (induct_tac "l")
 apply (simp (no_asm))
 apply (case_tac "list=[]")
@@ -108,7 +108,7 @@
  apply (erule exE)+
  apply hypsubst
 apply (simp del: reduce_Cons add: last_ind_on_first l_iff_red_nil)
-txt {* @{text "<--"} *}
+txt \<open>\<open><--\<close>\<close>
 apply (simp (no_asm) add: and_de_morgan_and_absorbe l_iff_red_nil)
 apply (induct_tac "l")
 apply (simp (no_asm))
@@ -120,7 +120,7 @@
 done
 
 
-text {* Main Lemma 2 for R_pkt in showing that reduce is refinement. *}
+text \<open>Main Lemma 2 for R_pkt in showing that reduce is refinement.\<close>
 lemma reduce_tl: "s~=[] ==>
      if hd(s)=hd(tl(s)) & tl(s)~=[] then
        reduce(tl(s))=reduce(s) else
@@ -132,23 +132,23 @@
 done
 
 
-subsection {* Channel Abstraction *}
+subsection \<open>Channel Abstraction\<close>
 
 declare split_if [split del]
 
 lemma channel_abstraction: "is_weak_ref_map reduce ch_ioa ch_fin_ioa"
 apply (simp (no_asm) add: is_weak_ref_map_def)
-txt {* main-part *}
+txt \<open>main-part\<close>
 apply (rule allI)+
 apply (rule imp_conj_lemma)
 apply (induct_tac "a")
-txt {* 2 cases *}
+txt \<open>2 cases\<close>
 apply (simp_all (no_asm) cong del: if_weak_cong add: externals_def)
-txt {* fst case *}
+txt \<open>fst case\<close>
  apply (rule impI)
  apply (rule disjI2)
 apply (rule reduce_hd)
-txt {* snd case *}
+txt \<open>snd case\<close>
  apply (rule impI)
  apply (erule conjE)+
  apply (erule disjE)
@@ -164,49 +164,49 @@
 declare split_if [split]
 
 lemma sender_abstraction: "is_weak_ref_map reduce srch_ioa srch_fin_ioa"
-apply (tactic {*
+apply (tactic \<open>
   simp_tac (put_simpset HOL_ss @{context}
     addsimps [@{thm srch_fin_ioa_def}, @{thm rsch_fin_ioa_def},
       @{thm srch_ioa_def}, @{thm rsch_ioa_def}, @{thm rename_through_pmap},
-      @{thm channel_abstraction}]) 1 *})
+      @{thm channel_abstraction}]) 1\<close>)
 done
 
 lemma receiver_abstraction: "is_weak_ref_map reduce rsch_ioa rsch_fin_ioa"
-apply (tactic {*
+apply (tactic \<open>
   simp_tac (put_simpset HOL_ss @{context}
     addsimps [@{thm srch_fin_ioa_def}, @{thm rsch_fin_ioa_def},
       @{thm srch_ioa_def}, @{thm rsch_ioa_def}, @{thm rename_through_pmap},
-      @{thm channel_abstraction}]) 1 *})
+      @{thm channel_abstraction}]) 1\<close>)
 done
 
 
-text {* 3 thms that do not hold generally! The lucky restriction here is
-   the absence of internal actions. *}
+text \<open>3 thms that do not hold generally! The lucky restriction here is
+   the absence of internal actions.\<close>
 lemma sender_unchanged: "is_weak_ref_map (%id. id) sender_ioa sender_ioa"
 apply (simp (no_asm) add: is_weak_ref_map_def)
-txt {* main-part *}
+txt \<open>main-part\<close>
 apply (rule allI)+
 apply (induct_tac a)
-txt {* 7 cases *}
+txt \<open>7 cases\<close>
 apply (simp_all (no_asm) add: externals_def)
 done
 
-text {* 2 copies of before *}
+text \<open>2 copies of before\<close>
 lemma receiver_unchanged: "is_weak_ref_map (%id. id) receiver_ioa receiver_ioa"
 apply (simp (no_asm) add: is_weak_ref_map_def)
-txt {* main-part *}
+txt \<open>main-part\<close>
 apply (rule allI)+
 apply (induct_tac a)
-txt {* 7 cases *}
+txt \<open>7 cases\<close>
 apply (simp_all (no_asm) add: externals_def)
 done
 
 lemma env_unchanged: "is_weak_ref_map (%id. id) env_ioa env_ioa"
 apply (simp (no_asm) add: is_weak_ref_map_def)
-txt {* main-part *}
+txt \<open>main-part\<close>
 apply (rule allI)+
 apply (induct_tac a)
-txt {* 7 cases *}
+txt \<open>7 cases\<close>
 apply (simp_all (no_asm) add: externals_def)
 done
 
@@ -218,7 +218,7 @@
 apply simp_all
 done
 
-text {* totally the same as before *}
+text \<open>totally the same as before\<close>
 lemma compat_single_fin_ch: "compatible srch_fin_ioa rsch_fin_ioa"
 apply (simp add: compatible_def Int_def)
 apply (rule set_eqI)
@@ -240,7 +240,7 @@
 apply simp_all
 done
 
-text {* 5 proofs totally the same as before *}
+text \<open>5 proofs totally the same as before\<close>
 lemma compat_rec_fin: "compatible receiver_ioa (srch_fin_ioa \<parallel> rsch_fin_ioa)"
 apply (simp del: del_simps
   add: compatible_def asig_of_par asig_comp_def actions_def Int_def)
@@ -291,13 +291,13 @@
 done
 
 
-text {* lemmata about externals of channels *}
+text \<open>lemmata about externals of channels\<close>
 lemma ext_single_ch: "externals(asig_of(srch_fin_ioa)) = externals(asig_of(srch_ioa)) &
     externals(asig_of(rsch_fin_ioa)) = externals(asig_of(rsch_ioa))"
   by (simp add: externals_def)
 
 
-subsection {* Soundness of Abstraction *}
+subsection \<open>Soundness of Abstraction\<close>
 
 lemmas ext_simps = externals_of_par ext_single_ch
   and compat_simps = compat_single_ch compat_single_fin_ch compat_rec
diff -r 1f2788fb0b8b -r f1599e98c4d0 src/HOL/HOLCF/IOA/ABP/Env.thy
--- a/src/HOL/HOLCF/IOA/ABP/Env.thy	Wed Dec 30 21:56:12 2015 +0100
+++ b/src/HOL/HOLCF/IOA/ABP/Env.thy	Wed Dec 30 21:57:52 2015 +0100
@@ -2,14 +2,14 @@
     Author:     Olaf Müller
 *)
 
-section {* The environment *}
+section \<open>The environment\<close>
 
 theory Env
 imports "~~/src/HOL/HOLCF/IOA/meta_theory/IOA" Action
 begin
 
 type_synonym
-  'm env_state = bool   -- {* give next bit to system *}
+  'm env_state = bool   \<comment> \<open>give next bit to system\<close>
 
 definition
   env_asig :: "'m action signature" where
diff -r 1f2788fb0b8b -r f1599e98c4d0 src/HOL/HOLCF/IOA/ABP/Impl.thy
--- a/src/HOL/HOLCF/IOA/ABP/Impl.thy	Wed Dec 30 21:56:12 2015 +0100
+++ b/src/HOL/HOLCF/IOA/ABP/Impl.thy	Wed Dec 30 21:57:52 2015 +0100
@@ -2,7 +2,7 @@
     Author:     Olaf Müller
 *)
 
-section {* The implementation *}
+section \<open>The implementation\<close>
 
 theory Impl
 imports Sender Receiver Abschannel
diff -r 1f2788fb0b8b -r f1599e98c4d0 src/HOL/HOLCF/IOA/ABP/Impl_finite.thy
--- a/src/HOL/HOLCF/IOA/ABP/Impl_finite.thy	Wed Dec 30 21:56:12 2015 +0100
+++ b/src/HOL/HOLCF/IOA/ABP/Impl_finite.thy	Wed Dec 30 21:57:52 2015 +0100
@@ -2,7 +2,7 @@
     Author:     Olaf Müller
 *)
 
-section {* The implementation *}
+section \<open>The implementation\<close>
 
 theory Impl_finite
 imports Sender Receiver Abschannel_finite
diff -r 1f2788fb0b8b -r f1599e98c4d0 src/HOL/HOLCF/IOA/ABP/Lemmas.thy
--- a/src/HOL/HOLCF/IOA/ABP/Lemmas.thy	Wed Dec 30 21:56:12 2015 +0100
+++ b/src/HOL/HOLCF/IOA/ABP/Lemmas.thy	Wed Dec 30 21:57:52 2015 +0100
@@ -6,7 +6,7 @@
 imports Main
 begin
 
-subsection {* Logic *}
+subsection \<open>Logic\<close>
 
 lemma and_de_morgan_and_absorbe: "(~(A&B)) = ((~A)&B| ~B)"
   by blast
@@ -18,7 +18,7 @@
   by blast
 
 
-subsection {* Sets *}
+subsection \<open>Sets\<close>
 
 lemma set_lemmas:
     "f(x) : (UN x. {f(x)})"
@@ -27,8 +27,8 @@
     "!!a. (!x y. a ~= f x y) ==> a ~: (UN x y. {f x y})"
   by auto
 
-text {* 2 Lemmas to add to @{text "set_lemmas"}, used also for action handling, 
-   namely for Intersections and the empty list (compatibility of IOA!). *}
+text \<open>2 Lemmas to add to \<open>set_lemmas\<close>, used also for action handling, 
+   namely for Intersections and the empty list (compatibility of IOA!).\<close>
 lemma singleton_set: "(UN b.{x. x=f(b)})= (UN b.{f(b)})"
   by blast
 
@@ -36,7 +36,7 @@
   by blast
 
 
-subsection {* Lists *}
+subsection \<open>Lists\<close>
 
 lemma cons_not_nil: "l ~= [] --> (? x xs. l = (x#xs))"
   by (induct l) simp_all
diff -r 1f2788fb0b8b -r f1599e98c4d0 src/HOL/HOLCF/IOA/ABP/Packet.thy
--- a/src/HOL/HOLCF/IOA/ABP/Packet.thy	Wed Dec 30 21:56:12 2015 +0100
+++ b/src/HOL/HOLCF/IOA/ABP/Packet.thy	Wed Dec 30 21:57:52 2015 +0100
@@ -2,7 +2,7 @@
     Author:     Olaf Müller
 *)
 
-section {* Packets *}
+section \<open>Packets\<close>
 
 theory Packet
 imports Main
diff -r 1f2788fb0b8b -r f1599e98c4d0 src/HOL/HOLCF/IOA/ABP/Receiver.thy
--- a/src/HOL/HOLCF/IOA/ABP/Receiver.thy	Wed Dec 30 21:56:12 2015 +0100
+++ b/src/HOL/HOLCF/IOA/ABP/Receiver.thy	Wed Dec 30 21:57:52 2015 +0100
@@ -2,14 +2,14 @@
     Author:     Olaf Müller
 *)
 
-section {* The implementation: receiver *}
+section \<open>The implementation: receiver\<close>
 
 theory Receiver
 imports "~~/src/HOL/HOLCF/IOA/meta_theory/IOA" Action Lemmas
 begin
 
 type_synonym
-  'm receiver_state = "'m list * bool"  -- {* messages, mode *}
+  'm receiver_state = "'m list * bool"  \<comment> \<open>messages, mode\<close>
 
 definition
   rq :: "'m receiver_state => 'm list" where
diff -r 1f2788fb0b8b -r f1599e98c4d0 src/HOL/HOLCF/IOA/ABP/Sender.thy
--- a/src/HOL/HOLCF/IOA/ABP/Sender.thy	Wed Dec 30 21:56:12 2015 +0100
+++ b/src/HOL/HOLCF/IOA/ABP/Sender.thy	Wed Dec 30 21:57:52 2015 +0100
@@ -2,14 +2,14 @@
     Author:     Olaf Müller
 *)
 
-section {* The implementation: sender *}
+section \<open>The implementation: sender\<close>
 
 theory Sender
 imports "~~/src/HOL/HOLCF/IOA/meta_theory/IOA" Action Lemmas
 begin
 
 type_synonym
-  'm sender_state = "'m list  *  bool"  -- {* messages, Alternating Bit *}
+  'm sender_state = "'m list  *  bool"  \<comment> \<open>messages, Alternating Bit\<close>
 
 definition
   sq :: "'m sender_state => 'm list" where
diff -r 1f2788fb0b8b -r f1599e98c4d0 src/HOL/HOLCF/IOA/ABP/Spec.thy
--- a/src/HOL/HOLCF/IOA/ABP/Spec.thy	Wed Dec 30 21:56:12 2015 +0100
+++ b/src/HOL/HOLCF/IOA/ABP/Spec.thy	Wed Dec 30 21:57:52 2015 +0100
@@ -2,7 +2,7 @@
     Author:     Olaf Müller
 *)
 
-section {* The specification of reliable transmission *}
+section \<open>The specification of reliable transmission\<close>
 
 theory Spec
 imports IOA Action
diff -r 1f2788fb0b8b -r f1599e98c4d0 src/HOL/HOLCF/IOA/NTP/Abschannel.thy
--- a/src/HOL/HOLCF/IOA/NTP/Abschannel.thy	Wed Dec 30 21:56:12 2015 +0100
+++ b/src/HOL/HOLCF/IOA/NTP/Abschannel.thy	Wed Dec 30 21:57:52 2015 +0100
@@ -2,7 +2,7 @@
     Author:     Olaf Müller
 *)
 
-section {* The (faulty) transmission channel (both directions) *}
+section \<open>The (faulty) transmission channel (both directions)\<close>
 
 theory Abschannel
 imports "~~/src/HOL/HOLCF/IOA/meta_theory/IOA" Action
diff -r 1f2788fb0b8b -r f1599e98c4d0 src/HOL/HOLCF/IOA/NTP/Action.thy
--- a/src/HOL/HOLCF/IOA/NTP/Action.thy	Wed Dec 30 21:56:12 2015 +0100
+++ b/src/HOL/HOLCF/IOA/NTP/Action.thy	Wed Dec 30 21:57:52 2015 +0100
@@ -2,7 +2,7 @@
     Author:     Tobias Nipkow & Konrad Slind
 *)
 
-section {* The set of all actions of the system *}
+section \<open>The set of all actions of the system\<close>
 
 theory Action
 imports Packet
diff -r 1f2788fb0b8b -r f1599e98c4d0 src/HOL/HOLCF/IOA/NTP/Correctness.thy
--- a/src/HOL/HOLCF/IOA/NTP/Correctness.thy	Wed Dec 30 21:56:12 2015 +0100
+++ b/src/HOL/HOLCF/IOA/NTP/Correctness.thy	Wed Dec 30 21:57:52 2015 +0100
@@ -2,7 +2,7 @@
     Author:     Tobias Nipkow & Konrad Slind
 *)
 
-section {* The main correctness proof: Impl implements Spec *}
+section \<open>The main correctness proof: Impl implements Spec\<close>
 
 theory Correctness
 imports Impl Spec
@@ -13,7 +13,7 @@
   "hom s = rq(rec(s)) @ (if rbit(rec s) = sbit(sen s) then sq(sen s)
                          else tl(sq(sen s)))"
 
-setup {* map_theory_claset (fn ctxt => ctxt delSWrapper "split_all_tac") *}
+setup \<open>map_theory_claset (fn ctxt => ctxt delSWrapper "split_all_tac")\<close>
 
 lemmas hom_ioas = Spec.ioa_def Spec.trans_def sender_trans_def receiver_trans_def impl_ioas
   and impl_asigs = sender_asig_def receiver_asig_def srch_asig_def rsch_asig_def
@@ -21,10 +21,10 @@
 declare split_paired_All [simp del]
 
 
-text {*
+text \<open>
   A lemma about restricting the action signature of the implementation
   to that of the specification.
-*}
+\<close>
 
 lemma externals_lemma: 
  "a:externals(asig_of(Automata.restrict impl_ioa (externals spec_sig))) =  
@@ -43,12 +43,12 @@
 
   apply (induct_tac "a")
   apply (simp_all (no_asm) add: actions_def asig_projections)
-  txt {* 2 *}
+  txt \<open>2\<close>
   apply (simp (no_asm) add: impl_ioas)
   apply (simp (no_asm) add: impl_asigs)
   apply (simp (no_asm) add: asig_of_par asig_comp_def asig_projections)
   apply (simp (no_asm) add: "transitions"(1) unfold_renaming)
-  txt {* 1 *}
+  txt \<open>1\<close>
   apply (simp (no_asm) add: impl_ioas)
   apply (simp (no_asm) add: impl_asigs)
   apply (simp (no_asm) add: asig_of_par asig_comp_def asig_projections)
@@ -57,7 +57,7 @@
 lemmas sels = sbit_def sq_def ssending_def rbit_def rq_def rsending_def
 
 
-text {* Proof of correctness *}
+text \<open>Proof of correctness\<close>
 lemma ntp_correct:
   "is_weak_ref_map hom (Automata.restrict impl_ioa (externals spec_sig)) spec_ioa"
 apply (unfold Spec.ioa_def is_weak_ref_map_def)
diff -r 1f2788fb0b8b -r f1599e98c4d0 src/HOL/HOLCF/IOA/NTP/Impl.thy
--- a/src/HOL/HOLCF/IOA/NTP/Impl.thy	Wed Dec 30 21:56:12 2015 +0100
+++ b/src/HOL/HOLCF/IOA/NTP/Impl.thy	Wed Dec 30 21:57:52 2015 +0100
@@ -2,7 +2,7 @@
     Author:     Tobias Nipkow & Konrad Slind
 *)
 
-section {* The implementation *}
+section \<open>The implementation\<close>
 
 theory Impl
 imports Sender Receiver Abschannel
@@ -59,7 +59,7 @@
 definition "inv4(s) == rbit(rec(s)) = (~sbit(sen(s))) --> sq(sen(s)) ~= []"
 
 
-subsection {* Invariants *}
+subsection \<open>Invariants\<close>
 
 declare le_SucI [simp]
 
@@ -101,7 +101,7 @@
 2) ss unfolds transition relations
 3) renname_ss unfolds transitions and the abstract channel *)
 
-ML {*
+ML \<open>
 val ss = simpset_of (@{context} addsimps @{thms "transitions"});
 val rename_ss = simpset_of (put_simpset ss @{context} addsimps @{thms unfold_renaming});
 
@@ -111,10 +111,10 @@
 fun tac_ren ctxt =
   asm_simp_tac (put_simpset rename_ss ctxt
     |> Simplifier.add_cong @{thm conj_cong} |> Splitter.add_split @{thm split_if})
-*}
+\<close>
 
 
-subsubsection {* Invariant 1 *}
+subsubsection \<open>Invariant 1\<close>
 
 lemma raw_inv1: "invariant impl_ioa inv1"
 
@@ -124,7 +124,7 @@
 
 apply (simp (no_asm) del: trans_of_par4 add: imp_conjR inv1_def)
 
-txt {* Split proof in two *}
+txt \<open>Split proof in two\<close>
 apply (rule conjI)
 
 (* First half *)
@@ -135,28 +135,28 @@
 apply (tactic "tac @{context} 1")
 apply (tactic "tac_ren @{context} 1")
 
-txt {* 5 + 1 *}
+txt \<open>5 + 1\<close>
 
 apply (tactic "tac @{context} 1")
 apply (tactic "tac_ren @{context} 1")
 
-txt {* 4 + 1 *}
-apply (tactic {* EVERY1[tac @{context}, tac @{context}, tac @{context}, tac @{context}] *})
+txt \<open>4 + 1\<close>
+apply (tactic \<open>EVERY1[tac @{context}, tac @{context}, tac @{context}, tac @{context}]\<close>)
 
 
-txt {* Now the other half *}
+txt \<open>Now the other half\<close>
 apply (simp add: Impl.inv1_def split del: split_if)
 apply (induct_tac a)
 apply (tactic "EVERY1 [tac @{context}, tac @{context}]")
 
-txt {* detour 1 *}
+txt \<open>detour 1\<close>
 apply (tactic "tac @{context} 1")
 apply (tactic "tac_ren @{context} 1")
 apply (rule impI)
 apply (erule conjE)+
 apply (simp (no_asm_simp) add: hdr_sum_def Multiset.count_def Multiset.countm_nonempty_def
   split add: split_if)
-txt {* detour 2 *}
+txt \<open>detour 2\<close>
 apply (tactic "tac @{context} 1")
 apply (tactic "tac_ren @{context} 1")
 apply (rule impI)
@@ -190,79 +190,79 @@
 
 
 
-subsubsection {* INVARIANT 2 *}
+subsubsection \<open>INVARIANT 2\<close>
 
 lemma raw_inv2: "invariant impl_ioa inv2"
 
   apply (rule invariantI1)
-  txt {* Base case *}
+  txt \<open>Base case\<close>
   apply (simp add: inv2_def receiver_projections sender_projections impl_ioas)
 
   apply (simp (no_asm_simp) add: impl_ioas split del: split_if)
   apply (induct_tac "a")
 
-  txt {* 10 cases. First 4 are simple, since state doesn't change *}
+  txt \<open>10 cases. First 4 are simple, since state doesn't change\<close>
 
-  ML_prf {* val tac2 = asm_full_simp_tac (put_simpset ss @{context} addsimps [@{thm inv2_def}]) *}
+  ML_prf \<open>val tac2 = asm_full_simp_tac (put_simpset ss @{context} addsimps [@{thm inv2_def}])\<close>
 
-  txt {* 10 - 7 *}
+  txt \<open>10 - 7\<close>
   apply (tactic "EVERY1 [tac2,tac2,tac2,tac2]")
-  txt {* 6 *}
-  apply (tactic {* forward_tac @{context} [rewrite_rule @{context} [@{thm Impl.inv1_def}]
-                               (@{thm raw_inv1} RS @{thm invariantE}) RS conjunct1] 1 *})
+  txt \<open>6\<close>
+  apply (tactic \<open>forward_tac @{context} [rewrite_rule @{context} [@{thm Impl.inv1_def}]
+                               (@{thm raw_inv1} RS @{thm invariantE}) RS conjunct1] 1\<close>)
 
-  txt {* 6 - 5 *}
+  txt \<open>6 - 5\<close>
   apply (tactic "EVERY1 [tac2,tac2]")
 
-  txt {* 4 *}
-  apply (tactic {* forward_tac @{context} [rewrite_rule @{context} [@{thm Impl.inv1_def}]
-                                (@{thm raw_inv1} RS @{thm invariantE}) RS conjunct1] 1 *})
+  txt \<open>4\<close>
+  apply (tactic \<open>forward_tac @{context} [rewrite_rule @{context} [@{thm Impl.inv1_def}]
+                                (@{thm raw_inv1} RS @{thm invariantE}) RS conjunct1] 1\<close>)
   apply (tactic "tac2 1")
 
-  txt {* 3 *}
-  apply (tactic {* forward_tac @{context} [rewrite_rule @{context} [@{thm Impl.inv1_def}]
-    (@{thm raw_inv1} RS @{thm invariantE})] 1 *})
+  txt \<open>3\<close>
+  apply (tactic \<open>forward_tac @{context} [rewrite_rule @{context} [@{thm Impl.inv1_def}]
+    (@{thm raw_inv1} RS @{thm invariantE})] 1\<close>)
 
   apply (tactic "tac2 1")
-  apply (tactic {* fold_goals_tac @{context} [rewrite_rule @{context} [@{thm Packet.hdr_def}]
-    (@{thm Impl.hdr_sum_def})] *})
+  apply (tactic \<open>fold_goals_tac @{context} [rewrite_rule @{context} [@{thm Packet.hdr_def}]
+    (@{thm Impl.hdr_sum_def})]\<close>)
   apply arith
 
-  txt {* 2 *}
+  txt \<open>2\<close>
   apply (tactic "tac2 1")
-  apply (tactic {* forward_tac @{context} [rewrite_rule @{context} [@{thm Impl.inv1_def}]
-                               (@{thm raw_inv1} RS @{thm invariantE}) RS conjunct1] 1 *})
+  apply (tactic \<open>forward_tac @{context} [rewrite_rule @{context} [@{thm Impl.inv1_def}]
+                               (@{thm raw_inv1} RS @{thm invariantE}) RS conjunct1] 1\<close>)
   apply (intro strip)
   apply (erule conjE)+
   apply simp
 
-  txt {* 1 *}
+  txt \<open>1\<close>
   apply (tactic "tac2 1")
-  apply (tactic {* forward_tac @{context} [rewrite_rule @{context} [@{thm Impl.inv1_def}]
-                               (@{thm raw_inv1} RS @{thm invariantE}) RS conjunct2] 1 *})
+  apply (tactic \<open>forward_tac @{context} [rewrite_rule @{context} [@{thm Impl.inv1_def}]
+                               (@{thm raw_inv1} RS @{thm invariantE}) RS conjunct2] 1\<close>)
   apply (intro strip)
   apply (erule conjE)+
-  apply (tactic {* fold_goals_tac @{context}
-    [rewrite_rule @{context} [@{thm Packet.hdr_def}] (@{thm Impl.hdr_sum_def})] *})
+  apply (tactic \<open>fold_goals_tac @{context}
+    [rewrite_rule @{context} [@{thm Packet.hdr_def}] (@{thm Impl.hdr_sum_def})]\<close>)
   apply simp
 
   done
 
 
-subsubsection {* INVARIANT 3 *}
+subsubsection \<open>INVARIANT 3\<close>
 
 lemma raw_inv3: "invariant impl_ioa inv3"
 
   apply (rule invariantI)
-  txt {* Base case *}
+  txt \<open>Base case\<close>
   apply (simp add: Impl.inv3_def receiver_projections sender_projections impl_ioas)
 
   apply (simp (no_asm_simp) add: impl_ioas split del: split_if)
   apply (induct_tac "a")
 
-  ML_prf {* val tac3 = asm_full_simp_tac (put_simpset ss @{context} addsimps [@{thm inv3_def}]) *}
+  ML_prf \<open>val tac3 = asm_full_simp_tac (put_simpset ss @{context} addsimps [@{thm inv3_def}])\<close>
 
-  txt {* 10 - 8 *}
+  txt \<open>10 - 8\<close>
 
   apply (tactic "EVERY1[tac3,tac3,tac3]")
 
@@ -272,29 +272,29 @@
   apply (erule exE)
   apply simp
 
-  txt {* 7 *}
+  txt \<open>7\<close>
   apply (tactic "tac3 1")
   apply (tactic "tac_ren @{context} 1")
   apply force
 
-  txt {* 6 - 3 *}
+  txt \<open>6 - 3\<close>
 
   apply (tactic "EVERY1[tac3,tac3,tac3,tac3]")
 
-  txt {* 2 *}
+  txt \<open>2\<close>
   apply (tactic "asm_full_simp_tac (put_simpset ss @{context}) 1")
   apply (simp (no_asm) add: inv3_def)
   apply (intro strip, (erule conjE)+)
   apply (rule imp_disjL [THEN iffD1])
   apply (rule impI)
-  apply (tactic {* forward_tac @{context} [rewrite_rule @{context} [@{thm Impl.inv2_def}]
-    (@{thm raw_inv2} RS @{thm invariantE})] 1 *})
+  apply (tactic \<open>forward_tac @{context} [rewrite_rule @{context} [@{thm Impl.inv2_def}]
+    (@{thm raw_inv2} RS @{thm invariantE})] 1\<close>)
   apply simp
   apply (erule conjE)+
   apply (rule_tac j = "count (ssent (sen s)) (~sbit (sen s))" and
     k = "count (rsent (rec s)) (sbit (sen s))" in le_trans)
-  apply (tactic {* forward_tac @{context} [rewrite_rule @{context} [@{thm inv1_def}]
-                                (@{thm raw_inv1} RS @{thm invariantE}) RS conjunct2] 1 *})
+  apply (tactic \<open>forward_tac @{context} [rewrite_rule @{context} [@{thm inv1_def}]
+                                (@{thm raw_inv1} RS @{thm invariantE}) RS conjunct2] 1\<close>)
   apply (simp add: hdr_sum_def Multiset.count_def)
   apply (rule add_le_mono)
   apply (rule countm_props)
@@ -303,56 +303,56 @@
   apply (simp (no_asm))
   apply assumption
 
-  txt {* 1 *}
+  txt \<open>1\<close>
   apply (tactic "tac3 1")
   apply (intro strip, (erule conjE)+)
   apply (rule imp_disjL [THEN iffD1])
   apply (rule impI)
-  apply (tactic {* forward_tac @{context} [rewrite_rule @{context} [@{thm Impl.inv2_def}]
-    (@{thm raw_inv2} RS @{thm invariantE})] 1 *})
+  apply (tactic \<open>forward_tac @{context} [rewrite_rule @{context} [@{thm Impl.inv2_def}]
+    (@{thm raw_inv2} RS @{thm invariantE})] 1\<close>)
   apply simp
   done
 
 
-subsubsection {* INVARIANT 4 *}
+subsubsection \<open>INVARIANT 4\<close>
 
 lemma raw_inv4: "invariant impl_ioa inv4"
 
   apply (rule invariantI)
-  txt {* Base case *}
+  txt \<open>Base case\<close>
   apply (simp add: Impl.inv4_def receiver_projections sender_projections impl_ioas)
 
   apply (simp (no_asm_simp) add: impl_ioas split del: split_if)
   apply (induct_tac "a")
 
-  ML_prf {* val tac4 =  asm_full_simp_tac (put_simpset ss @{context} addsimps [@{thm inv4_def}]) *}
+  ML_prf \<open>val tac4 =  asm_full_simp_tac (put_simpset ss @{context} addsimps [@{thm inv4_def}])\<close>
 
-  txt {* 10 - 2 *}
+  txt \<open>10 - 2\<close>
 
   apply (tactic "EVERY1[tac4,tac4,tac4,tac4,tac4,tac4,tac4,tac4,tac4]")
 
-  txt {* 2 b *}
+  txt \<open>2 b\<close>
 
   apply (intro strip, (erule conjE)+)
-  apply (tactic {* forward_tac @{context} [rewrite_rule @{context} [@{thm Impl.inv2_def}]
-                               (@{thm raw_inv2} RS @{thm invariantE})] 1 *})
+  apply (tactic \<open>forward_tac @{context} [rewrite_rule @{context} [@{thm Impl.inv2_def}]
+                               (@{thm raw_inv2} RS @{thm invariantE})] 1\<close>)
   apply simp
 
-  txt {* 1 *}
+  txt \<open>1\<close>
   apply (tactic "tac4 1")
   apply (intro strip, (erule conjE)+)
   apply (rule ccontr)
-  apply (tactic {* forward_tac @{context} [rewrite_rule @{context} [@{thm Impl.inv2_def}]
-                               (@{thm raw_inv2} RS @{thm invariantE})] 1 *})
-  apply (tactic {* forward_tac @{context} [rewrite_rule @{context} [@{thm Impl.inv3_def}]
-                               (@{thm raw_inv3} RS @{thm invariantE})] 1 *})
+  apply (tactic \<open>forward_tac @{context} [rewrite_rule @{context} [@{thm Impl.inv2_def}]
+                               (@{thm raw_inv2} RS @{thm invariantE})] 1\<close>)
+  apply (tactic \<open>forward_tac @{context} [rewrite_rule @{context} [@{thm Impl.inv3_def}]
+                               (@{thm raw_inv3} RS @{thm invariantE})] 1\<close>)
   apply simp
   apply (rename_tac m, erule_tac x = "m" in allE)
   apply simp
   done
 
 
-text {* rebind them *}
+text \<open>rebind them\<close>
 
 lemmas inv1 = raw_inv1 [THEN invariantE, unfolded inv1_def]
   and inv2 = raw_inv2 [THEN invariantE, unfolded inv2_def]
diff -r 1f2788fb0b8b -r f1599e98c4d0 src/HOL/HOLCF/IOA/NTP/Lemmas.thy
--- a/src/HOL/HOLCF/IOA/NTP/Lemmas.thy	Wed Dec 30 21:56:12 2015 +0100
+++ b/src/HOL/HOLCF/IOA/NTP/Lemmas.thy	Wed Dec 30 21:57:52 2015 +0100
@@ -6,13 +6,13 @@
 imports Main
 begin
 
-subsubsection {* Logic *}
+subsubsection \<open>Logic\<close>
 
 lemma neg_flip: "(X = (~ Y)) = ((~X) = Y)"
   by blast
 
 
-subsection {* Sets *}
+subsection \<open>Sets\<close>
 
 lemma set_lemmas:
   "f(x) : (UN x. {f(x)})"
@@ -22,7 +22,7 @@
   by auto
 
 
-subsection {* Arithmetic *}
+subsection \<open>Arithmetic\<close>
 
 lemma pred_suc: "0<x ==> (x - 1 = y) = (x = Suc(y))"
   by (simp add: diff_Suc split add: nat.split)
diff -r 1f2788fb0b8b -r f1599e98c4d0 src/HOL/HOLCF/IOA/NTP/Multiset.thy
--- a/src/HOL/HOLCF/IOA/NTP/Multiset.thy	Wed Dec 30 21:56:12 2015 +0100
+++ b/src/HOL/HOLCF/IOA/NTP/Multiset.thy	Wed Dec 30 21:57:52 2015 +0100
@@ -2,7 +2,7 @@
     Author:     Tobias Nipkow & Konrad Slind
 *)
 
-section {* Axiomatic multisets *}
+section \<open>Axiomatic multisets\<close>
 
 theory Multiset
 imports Lemmas
diff -r 1f2788fb0b8b -r f1599e98c4d0 src/HOL/HOLCF/IOA/NTP/Packet.thy
--- a/src/HOL/HOLCF/IOA/NTP/Packet.thy	Wed Dec 30 21:56:12 2015 +0100
+++ b/src/HOL/HOLCF/IOA/NTP/Packet.thy	Wed Dec 30 21:57:52 2015 +0100
@@ -18,7 +18,7 @@
   "msg == snd"
 
 
-text {* Instantiation of a tautology? *}
+text \<open>Instantiation of a tautology?\<close>
 lemma eq_packet_imp_eq_hdr: "!x. x = packet --> hdr(x) = hdr(packet)"
   by simp
 
diff -r 1f2788fb0b8b -r f1599e98c4d0 src/HOL/HOLCF/IOA/NTP/Receiver.thy
--- a/src/HOL/HOLCF/IOA/NTP/Receiver.thy	Wed Dec 30 21:56:12 2015 +0100
+++ b/src/HOL/HOLCF/IOA/NTP/Receiver.thy	Wed Dec 30 21:57:52 2015 +0100
@@ -2,7 +2,7 @@
     Author:     Tobias Nipkow & Konrad Slind
 *)
 
-section {* The implementation: receiver *}
+section \<open>The implementation: receiver\<close>
 
 theory Receiver
 imports "~~/src/HOL/HOLCF/IOA/meta_theory/IOA" Action
diff -r 1f2788fb0b8b -r f1599e98c4d0 src/HOL/HOLCF/IOA/NTP/Sender.thy
--- a/src/HOL/HOLCF/IOA/NTP/Sender.thy	Wed Dec 30 21:56:12 2015 +0100
+++ b/src/HOL/HOLCF/IOA/NTP/Sender.thy	Wed Dec 30 21:57:52 2015 +0100
@@ -2,7 +2,7 @@
     Author:     Tobias Nipkow & Konrad Slind
 *)
 
-section {* The implementation: sender *}
+section \<open>The implementation: sender\<close>
 
 theory Sender
 imports "~~/src/HOL/HOLCF/IOA/meta_theory/IOA" Action
diff -r 1f2788fb0b8b -r f1599e98c4d0 src/HOL/HOLCF/IOA/NTP/Spec.thy
--- a/src/HOL/HOLCF/IOA/NTP/Spec.thy	Wed Dec 30 21:56:12 2015 +0100
+++ b/src/HOL/HOLCF/IOA/NTP/Spec.thy	Wed Dec 30 21:57:52 2015 +0100
@@ -2,7 +2,7 @@
     Author:     Tobias Nipkow & Konrad Slind
 *)
 
-section {* The specification of reliable transmission *}
+section \<open>The specification of reliable transmission\<close>
 
 theory Spec
 imports "~~/src/HOL/HOLCF/IOA/meta_theory/IOA" Action
diff -r 1f2788fb0b8b -r f1599e98c4d0 src/HOL/HOLCF/IOA/Storage/Action.thy
--- a/src/HOL/HOLCF/IOA/Storage/Action.thy	Wed Dec 30 21:56:12 2015 +0100
+++ b/src/HOL/HOLCF/IOA/Storage/Action.thy	Wed Dec 30 21:57:52 2015 +0100
@@ -2,7 +2,7 @@
     Author:     Olaf Müller
 *)
 
-section {* The set of all actions of the system *}
+section \<open>The set of all actions of the system\<close>
 
 theory Action
 imports Main
diff -r 1f2788fb0b8b -r f1599e98c4d0 src/HOL/HOLCF/IOA/Storage/Correctness.thy
--- a/src/HOL/HOLCF/IOA/Storage/Correctness.thy	Wed Dec 30 21:56:12 2015 +0100
+++ b/src/HOL/HOLCF/IOA/Storage/Correctness.thy	Wed Dec 30 21:57:52 2015 +0100
@@ -2,7 +2,7 @@
     Author:     Olaf Müller
 *)
 
-section {* Correctness Proof *}
+section \<open>Correctness Proof\<close>
 
 theory Correctness
 imports SimCorrectness Spec Impl
@@ -30,29 +30,29 @@
       "is_simulation sim_relation impl_ioa spec_ioa"
 apply (simp (no_asm) add: is_simulation_def)
 apply (rule conjI)
-txt {* start states *}
+txt \<open>start states\<close>
 apply (auto)[1]
 apply (rule_tac x = " ({},False) " in exI)
 apply (simp add: sim_relation_def starts_of_def spec_ioa_def impl_ioa_def)
-txt {* main-part *}
+txt \<open>main-part\<close>
 apply (rule allI)+
 apply (rule imp_conj_lemma)
 apply (rename_tac k b used c k' b' a)
 apply (induct_tac "a")
 apply (simp_all (no_asm) add: sim_relation_def impl_ioa_def impl_trans_def trans_of_def)
 apply auto
-txt {* NEW *}
+txt \<open>NEW\<close>
 apply (rule_tac x = "(used,True)" in exI)
 apply simp
 apply (rule transition_is_ex)
 apply (simp (no_asm) add: spec_ioa_def spec_trans_def trans_of_def)
-txt {* LOC *}
+txt \<open>LOC\<close>
 apply (rule_tac x = " (used Un {k},False) " in exI)
 apply (simp add: less_SucI)
 apply (rule transition_is_ex)
 apply (simp (no_asm) add: spec_ioa_def spec_trans_def trans_of_def)
 apply fast
-txt {* FREE *}
+txt \<open>FREE\<close>
 apply (rename_tac nat, rule_tac x = " (used - {nat},c) " in exI)
 apply simp
 apply (rule transition_is_ex)
diff -r 1f2788fb0b8b -r f1599e98c4d0 src/HOL/HOLCF/IOA/Storage/Impl.thy
--- a/src/HOL/HOLCF/IOA/Storage/Impl.thy	Wed Dec 30 21:56:12 2015 +0100
+++ b/src/HOL/HOLCF/IOA/Storage/Impl.thy	Wed Dec 30 21:57:52 2015 +0100
@@ -2,7 +2,7 @@
     Author:     Olaf Müller
 *)
 
-section {* The implementation of a memory *}
+section \<open>The implementation of a memory\<close>
 
 theory Impl
 imports IOA Action
diff -r 1f2788fb0b8b -r f1599e98c4d0 src/HOL/HOLCF/IOA/Storage/Spec.thy
--- a/src/HOL/HOLCF/IOA/Storage/Spec.thy	Wed Dec 30 21:56:12 2015 +0100
+++ b/src/HOL/HOLCF/IOA/Storage/Spec.thy	Wed Dec 30 21:57:52 2015 +0100
@@ -2,7 +2,7 @@
     Author:     Olaf Müller
 *)
 
-section {* The specification of a memory *}
+section \<open>The specification of a memory\<close>
 
 theory Spec
 imports "~~/src/HOL/HOLCF/IOA/meta_theory/IOA" Action
diff -r 1f2788fb0b8b -r f1599e98c4d0 src/HOL/HOLCF/IOA/ex/TrivEx.thy
--- a/src/HOL/HOLCF/IOA/ex/TrivEx.thy	Wed Dec 30 21:56:12 2015 +0100
+++ b/src/HOL/HOLCF/IOA/ex/TrivEx.thy	Wed Dec 30 21:57:52 2015 +0100
@@ -2,7 +2,7 @@
     Author:     Olaf Müller
 *)
 
-section {* Trivial Abstraction Example *}
+section \<open>Trivial Abstraction Example\<close>
 
 theory TrivEx
 imports Abstraction
@@ -51,9 +51,9 @@
   "is_abstraction h_abs C_ioa A_ioa"
 apply (unfold is_abstraction_def)
 apply (rule conjI)
-txt {* start states *}
+txt \<open>start states\<close>
 apply (simp (no_asm) add: h_abs_def starts_of_def C_ioa_def A_ioa_def)
-txt {* step case *}
+txt \<open>step case\<close>
 apply (rule allI)+
 apply (rule imp_conj_lemma)
 apply (simp (no_asm) add: trans_of_def C_ioa_def A_ioa_def C_trans_def A_trans_def)
diff -r 1f2788fb0b8b -r f1599e98c4d0 src/HOL/HOLCF/IOA/ex/TrivEx2.thy
--- a/src/HOL/HOLCF/IOA/ex/TrivEx2.thy	Wed Dec 30 21:56:12 2015 +0100
+++ b/src/HOL/HOLCF/IOA/ex/TrivEx2.thy	Wed Dec 30 21:57:52 2015 +0100
@@ -2,7 +2,7 @@
     Author:     Olaf Müller
 *)
 
-section {* Trivial Abstraction Example with fairness *}
+section \<open>Trivial Abstraction Example with fairness\<close>
 
 theory TrivEx2
 imports IOA Abstraction
@@ -58,9 +58,9 @@
 "is_abstraction h_abs C_ioa A_ioa"
 apply (unfold is_abstraction_def)
 apply (rule conjI)
-txt {* start states *}
+txt \<open>start states\<close>
 apply (simp (no_asm) add: h_abs_def starts_of_def C_ioa_def A_ioa_def)
-txt {* step case *}
+txt \<open>step case\<close>
 apply (rule allI)+
 apply (rule imp_conj_lemma)
 apply (simp (no_asm) add: trans_of_def C_ioa_def A_ioa_def C_trans_def A_trans_def)
@@ -81,9 +81,9 @@
 "is_live_abstraction h_abs (C_ioa, WF C_ioa {INC}) (A_ioa, WF A_ioa {INC})"
 apply (unfold is_live_abstraction_def)
 apply auto
-txt {* is_abstraction *}
+txt \<open>is_abstraction\<close>
 apply (rule h_abs_is_abstraction)
-txt {* temp_weakening *}
+txt \<open>temp_weakening\<close>
 apply abstraction
 apply (erule Enabled_implication)
 done
diff -r 1f2788fb0b8b -r f1599e98c4d0 src/HOL/HOLCF/IOA/meta_theory/Abstraction.thy
--- a/src/HOL/HOLCF/IOA/meta_theory/Abstraction.thy	Wed Dec 30 21:56:12 2015 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/Abstraction.thy	Wed Dec 30 21:57:52 2015 +0100
@@ -2,7 +2,7 @@
     Author:     Olaf Müller
 *)
 
-section {* Abstraction Theory -- tailored for I/O automata *}
+section \<open>Abstraction Theory -- tailored for I/O automata\<close>
 
 theory Abstraction
 imports LiveIOA
@@ -14,7 +14,7 @@
   cex_abs :: "('s1 => 's2) => ('a,'s1)execution => ('a,'s2)execution" where
   "cex_abs f ex = (f (fst ex), Map (%(a,t). (a,f t))$(snd ex))"
 definition
-  -- {* equals cex_abs on Sequences -- after ex2seq application *}
+  \<comment> \<open>equals cex_abs on Sequences -- after ex2seq application\<close>
   cex_absSeq :: "('s1 => 's2) => ('a option,'s1)transition Seq => ('a option,'s2)transition Seq" where
   "cex_absSeq f = (%s. Map (%(s,a,t). (f s,a,f t))$s)"
 
@@ -102,8 +102,8 @@
   --> is_exec_frag A (cex_abs h (s,xs))"
 apply (unfold cex_abs_def)
 apply simp
-apply (tactic {* pair_induct_tac @{context} "xs" [@{thm is_exec_frag_def}] 1 *})
-txt {* main case *}
+apply (tactic \<open>pair_induct_tac @{context} "xs" [@{thm is_exec_frag_def}] 1\<close>)
+txt \<open>main case\<close>
 apply (auto dest: reachable.reachable_n simp add: is_abstraction_def)
 done
 
@@ -112,10 +112,10 @@
 apply (simp add: weakeningIOA_def)
 apply auto
 apply (simp add: executions_def)
-txt {* start state *}
+txt \<open>start state\<close>
 apply (rule conjI)
 apply (simp add: is_abstraction_def cex_abs_def)
-txt {* is-execution-fragment *}
+txt \<open>is-execution-fragment\<close>
 apply (erule exec_frag_abstraction)
 apply (simp add: reachable.reachable_0)
 done
@@ -202,7 +202,7 @@
          ==> mk_trace C$xs = mk_trace A$(snd (cex_abs f (s,xs)))"
 apply (unfold cex_abs_def mk_trace_def filter_act_def)
 apply simp
-apply (tactic {* pair_induct_tac @{context} "xs" [] 1 *})
+apply (tactic \<open>pair_induct_tac @{context} "xs" [] 1\<close>)
 done
 
 
@@ -218,13 +218,13 @@
 apply (rule_tac x = "cex_abs h ex" in exI)
 apply auto
   (* Traces coincide *)
-  apply (tactic {* pair_tac @{context} "ex" 1 *})
+  apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
   apply (rule traces_coincide_abs)
   apply (simp (no_asm) add: externals_def)
   apply (auto)[1]
 
   (* cex_abs is execution *)
-  apply (tactic {* pair_tac @{context} "ex" 1 *})
+  apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
   apply (simp add: executions_def)
   (* start state *)
   apply (rule conjI)
@@ -235,7 +235,7 @@
 
  (* Liveness *)
 apply (simp add: temp_weakening_def2)
- apply (tactic {* pair_tac @{context} "ex" 1 *})
+ apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
 done
 
 (* FIX: NAch Traces.ML bringen *)
@@ -348,29 +348,29 @@
 done
 
 
-subsubsection {* Box *}
+subsubsection \<open>Box\<close>
 
 (* FIX: should be same as nil_is_Conc2 when all nils are turned to right side !! *)
 lemma UU_is_Conc: "(UU = x @@ y) = (((x::'a Seq)= UU) | (x=nil & y=UU))"
-apply (tactic {* Seq_case_simp_tac @{context} "x" 1 *})
+apply (tactic \<open>Seq_case_simp_tac @{context} "x" 1\<close>)
 done
 
 lemma ex2seqConc [rule_format]:
 "Finite s1 -->
   (! ex. (s~=nil & s~=UU & ex2seq ex = s1 @@ s) --> (? ex'. s = ex2seq ex'))"
 apply (rule impI)
-apply (tactic {* Seq_Finite_induct_tac @{context} 1 *})
+apply (tactic \<open>Seq_Finite_induct_tac @{context} 1\<close>)
 apply blast
 (* main case *)
 apply clarify
-apply (tactic {* pair_tac @{context} "ex" 1 *})
-apply (tactic {* Seq_case_simp_tac @{context} "x2" 1 *})
+apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
+apply (tactic \<open>Seq_case_simp_tac @{context} "x2" 1\<close>)
 (* UU case *)
 apply (simp add: nil_is_Conc)
 (* nil case *)
 apply (simp add: nil_is_Conc)
 (* cons case *)
-apply (tactic {* pair_tac @{context} "aa" 1 *})
+apply (tactic \<open>pair_tac @{context} "aa" 1\<close>)
 apply auto
 done
 
@@ -388,11 +388,11 @@
 (* FIX: NAch Sequence.ML bringen *)
 
 lemma Mapnil: "(Map f$s = nil) = (s=nil)"
-apply (tactic {* Seq_case_simp_tac @{context} "s" 1 *})
+apply (tactic \<open>Seq_case_simp_tac @{context} "s" 1\<close>)
 done
 
 lemma MapUU: "(Map f$s = UU) = (s=UU)"
-apply (tactic {* Seq_case_simp_tac @{context} "s" 1 *})
+apply (tactic \<open>Seq_case_simp_tac @{context} "s" 1\<close>)
 done
 
 
@@ -422,7 +422,7 @@
 done
 
 
-subsubsection {* Init *}
+subsubsection \<open>Init\<close>
 
 lemma strength_Init:
 "[| state_strengthening P Q h |]
@@ -430,35 +430,35 @@
 apply (unfold temp_strengthening_def state_strengthening_def
   temp_sat_def satisfies_def Init_def unlift_def)
 apply auto
-apply (tactic {* pair_tac @{context} "ex" 1 *})
-apply (tactic {* Seq_case_simp_tac @{context} "x2" 1 *})
-apply (tactic {* pair_tac @{context} "a" 1 *})
+apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
+apply (tactic \<open>Seq_case_simp_tac @{context} "x2" 1\<close>)
+apply (tactic \<open>pair_tac @{context} "a" 1\<close>)
 done
 
 
-subsubsection {* Next *}
+subsubsection \<open>Next\<close>
 
 lemma TL_ex2seq_UU:
 "(TL$(ex2seq (cex_abs h ex))=UU) = (TL$(ex2seq ex)=UU)"
-apply (tactic {* pair_tac @{context} "ex" 1 *})
-apply (tactic {* Seq_case_simp_tac @{context} "x2" 1 *})
-apply (tactic {* pair_tac @{context} "a" 1 *})
-apply (tactic {* Seq_case_simp_tac @{context} "s" 1 *})
-apply (tactic {* pair_tac @{context} "a" 1 *})
+apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
+apply (tactic \<open>Seq_case_simp_tac @{context} "x2" 1\<close>)
+apply (tactic \<open>pair_tac @{context} "a" 1\<close>)
+apply (tactic \<open>Seq_case_simp_tac @{context} "s" 1\<close>)
+apply (tactic \<open>pair_tac @{context} "a" 1\<close>)
 done
 
 lemma TL_ex2seq_nil:
 "(TL$(ex2seq (cex_abs h ex))=nil) = (TL$(ex2seq ex)=nil)"
-apply (tactic {* pair_tac @{context} "ex" 1 *})
-apply (tactic {* Seq_case_simp_tac @{context} "x2" 1 *})
-apply (tactic {* pair_tac @{context} "a" 1 *})
-apply (tactic {* Seq_case_simp_tac @{context} "s" 1 *})
-apply (tactic {* pair_tac @{context} "a" 1 *})
+apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
+apply (tactic \<open>Seq_case_simp_tac @{context} "x2" 1\<close>)
+apply (tactic \<open>pair_tac @{context} "a" 1\<close>)
+apply (tactic \<open>Seq_case_simp_tac @{context} "s" 1\<close>)
+apply (tactic \<open>pair_tac @{context} "a" 1\<close>)
 done
 
 (* FIX: put to Sequence Lemmas *)
 lemma MapTL: "Map f$(TL$s) = TL$(Map f$s)"
-apply (tactic {* Seq_induct_tac @{context} "s" [] 1 *})
+apply (tactic \<open>Seq_induct_tac @{context} "s" [] 1\<close>)
 done
 
 (* important property of cex_absSeq: As it is a 1to1 correspondence,
@@ -473,19 +473,19 @@
 (* important property of ex2seq: can be shiftet, as defined "pointwise" *)
 
 lemma TLex2seq: "[| (snd ex)~=UU ; (snd ex)~=nil |] ==> (? ex'. TL$(ex2seq ex) = ex2seq ex')"
-apply (tactic {* pair_tac @{context} "ex" 1 *})
-apply (tactic {* Seq_case_simp_tac @{context} "x2" 1 *})
-apply (tactic {* pair_tac @{context} "a" 1 *})
+apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
+apply (tactic \<open>Seq_case_simp_tac @{context} "x2" 1\<close>)
+apply (tactic \<open>pair_tac @{context} "a" 1\<close>)
 apply auto
 done
 
 
 lemma ex2seqnilTL: "(TL$(ex2seq ex)~=nil) = ((snd ex)~=nil & (snd ex)~=UU)"
-apply (tactic {* pair_tac @{context} "ex" 1 *})
-apply (tactic {* Seq_case_simp_tac @{context} "x2" 1 *})
-apply (tactic {* pair_tac @{context} "a" 1 *})
-apply (tactic {* Seq_case_simp_tac @{context} "s" 1 *})
-apply (tactic {* pair_tac @{context} "a" 1 *})
+apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
+apply (tactic \<open>Seq_case_simp_tac @{context} "x2" 1\<close>)
+apply (tactic \<open>pair_tac @{context} "a" 1\<close>)
+apply (tactic \<open>Seq_case_simp_tac @{context} "s" 1\<close>)
+apply (tactic \<open>pair_tac @{context} "a" 1\<close>)
 done
 
 
@@ -508,7 +508,7 @@
 done
 
 
-text {* Localizing Temporal Weakenings     - 2 *}
+text \<open>Localizing Temporal Weakenings     - 2\<close>
 
 lemma weak_Init:
 "[| state_weakening P Q h |]
@@ -516,13 +516,13 @@
 apply (simp add: temp_weakening_def2 state_weakening_def2
   temp_sat_def satisfies_def Init_def unlift_def)
 apply auto
-apply (tactic {* pair_tac @{context} "ex" 1 *})
-apply (tactic {* Seq_case_simp_tac @{context} "x2" 1 *})
-apply (tactic {* pair_tac @{context} "a" 1 *})
+apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
+apply (tactic \<open>Seq_case_simp_tac @{context} "x2" 1\<close>)
+apply (tactic \<open>pair_tac @{context} "a" 1\<close>)
 done
 
 
-text {* Localizing Temproal Strengthenings - 3 *}
+text \<open>Localizing Temproal Strengthenings - 3\<close>
 
 lemma strength_Diamond:
 "[| temp_strengthening P Q h |]
@@ -544,7 +544,7 @@
 done
 
 
-text {* Localizing Temporal Weakenings - 3 *}
+text \<open>Localizing Temporal Weakenings - 3\<close>
 
 lemma weak_Diamond:
 "[| temp_weakening P Q h |]
@@ -602,13 +602,13 @@
   strength_IMPLIES strength_Box strength_Next strength_Init
   strength_Diamond strength_Leadsto weak_WF weak_SF
 
-ML {*
+ML \<open>
 fun abstraction_tac ctxt =
   SELECT_GOAL (auto_tac
     (ctxt addSIs @{thms weak_strength_lemmas}
       addsimps [@{thm state_strengthening_def}, @{thm state_weakening_def}]))
-*}
+\<close>
 
-method_setup abstraction = {* Scan.succeed (SIMPLE_METHOD' o abstraction_tac) *}
+method_setup abstraction = \<open>Scan.succeed (SIMPLE_METHOD' o abstraction_tac)\<close>
 
 end
diff -r 1f2788fb0b8b -r f1599e98c4d0 src/HOL/HOLCF/IOA/meta_theory/Asig.thy
--- a/src/HOL/HOLCF/IOA/meta_theory/Asig.thy	Wed Dec 30 21:56:12 2015 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/Asig.thy	Wed Dec 30 21:57:52 2015 +0100
@@ -2,7 +2,7 @@
     Author:     Olaf Müller, Tobias Nipkow & Konrad Slind
 *)
 
-section {* Action signatures *}
+section \<open>Action signatures\<close>
 
 theory Asig
 imports Main
diff -r 1f2788fb0b8b -r f1599e98c4d0 src/HOL/HOLCF/IOA/meta_theory/Automata.thy
--- a/src/HOL/HOLCF/IOA/meta_theory/Automata.thy	Wed Dec 30 21:56:12 2015 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/Automata.thy	Wed Dec 30 21:57:52 2015 +0100
@@ -2,7 +2,7 @@
     Author:     Olaf Müller, Konrad Slind, Tobias Nipkow
 *)
 
-section {* The I/O automata of Lynch and Tuttle in HOLCF *}
+section \<open>The I/O automata of Lynch and Tuttle in HOLCF\<close>
 
 theory Automata
 imports Asig
diff -r 1f2788fb0b8b -r f1599e98c4d0 src/HOL/HOLCF/IOA/meta_theory/CompoExecs.thy
--- a/src/HOL/HOLCF/IOA/meta_theory/CompoExecs.thy	Wed Dec 30 21:56:12 2015 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/CompoExecs.thy	Wed Dec 30 21:57:52 2015 +0100
@@ -2,7 +2,7 @@
     Author:     Olaf Müller
 *)
 
-section {* Compositionality on Execution level *}
+section \<open>Compositionality on Execution level\<close>
 
 theory CompoExecs
 imports Traces
@@ -215,7 +215,7 @@
        -->  is_exec_frag A (fst s, Filter_ex2 (asig_of A)$(ProjA2$xs)) &
             is_exec_frag B (snd s, Filter_ex2 (asig_of B)$(ProjB2$xs))"
 
-apply (tactic {* pair_induct_tac @{context} "xs" [@{thm is_exec_frag_def}] 1 *})
+apply (tactic \<open>pair_induct_tac @{context} "xs" [@{thm is_exec_frag_def}] 1\<close>)
 (* main case *)
 apply (auto simp add: trans_of_defs2)
 done
@@ -229,8 +229,8 @@
        --> stutter (asig_of A) (fst s,ProjA2$xs)  &
            stutter (asig_of B) (snd s,ProjB2$xs)"
 
-apply (tactic {* pair_induct_tac @{context} "xs"
-  [@{thm stutter_def}, @{thm is_exec_frag_def}] 1 *})
+apply (tactic \<open>pair_induct_tac @{context} "xs"
+  [@{thm stutter_def}, @{thm is_exec_frag_def}] 1\<close>)
 (* main case *)
 apply (auto simp add: trans_of_defs2)
 done
@@ -243,8 +243,8 @@
 lemma lemma_1_1c: "!s. (is_exec_frag (A\<parallel>B) (s,xs)
    --> Forall (%x. fst x:act (A\<parallel>B)) xs)"
 
-apply (tactic {* pair_induct_tac @{context} "xs" [@{thm Forall_def}, @{thm sforall_def},
-  @{thm is_exec_frag_def}] 1 *})
+apply (tactic \<open>pair_induct_tac @{context} "xs" [@{thm Forall_def}, @{thm sforall_def},
+  @{thm is_exec_frag_def}] 1\<close>)
 (* main case *)
 apply auto
 apply (simp add: trans_of_defs2 actions_asig_comp asig_of_par)
@@ -263,13 +263,13 @@
      Forall (%x. fst x:act (A\<parallel>B)) xs
      --> is_exec_frag (A\<parallel>B) (s,xs)"
 
-apply (tactic {* pair_induct_tac @{context} "xs" [@{thm Forall_def}, @{thm sforall_def},
-  @{thm is_exec_frag_def}, @{thm stutter_def}] 1 *})
+apply (tactic \<open>pair_induct_tac @{context} "xs" [@{thm Forall_def}, @{thm sforall_def},
+  @{thm is_exec_frag_def}, @{thm stutter_def}] 1\<close>)
 apply (auto simp add: trans_of_defs1 actions_asig_comp asig_of_par)
 done
 
 
-subsection {* COMPOSITIONALITY on EXECUTION Level -- Main Theorem *}
+subsection \<open>COMPOSITIONALITY on EXECUTION Level -- Main Theorem\<close>
 
 lemma compositionality_ex:
 "(ex:executions(A\<parallel>B)) =
@@ -279,7 +279,7 @@
   Forall (%x. fst x:act (A\<parallel>B)) (snd ex))"
 
 apply (simp (no_asm) add: executions_def ProjB_def Filter_ex_def ProjA_def starts_of_par)
-apply (tactic {* pair_tac @{context} "ex" 1 *})
+apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
 apply (rule iffI)
 (* ==>  *)
 apply (erule conjE)+
@@ -290,7 +290,7 @@
 done
 
 
-subsection {* COMPOSITIONALITY on EXECUTION Level -- for Modules *}
+subsection \<open>COMPOSITIONALITY on EXECUTION Level -- for Modules\<close>
 
 lemma compositionality_ex_modules:
   "Execs (A\<parallel>B) = par_execs (Execs A) (Execs B)"
diff -r 1f2788fb0b8b -r f1599e98c4d0 src/HOL/HOLCF/IOA/meta_theory/CompoScheds.thy
--- a/src/HOL/HOLCF/IOA/meta_theory/CompoScheds.thy	Wed Dec 30 21:56:12 2015 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/CompoScheds.thy	Wed Dec 30 21:57:52 2015 +0100
@@ -2,7 +2,7 @@
     Author:     Olaf Müller
 *)
 
-section {* Compositionality on Schedule level *}
+section \<open>Compositionality on Schedule level\<close>
 
 theory CompoScheds
 imports CompoExecs
@@ -149,7 +149,7 @@
   mkex2_cons_2 [simp] mkex2_cons_3 [simp]
 
 
-subsection {* mkex *}
+subsection \<open>mkex\<close>
 
 lemma mkex_UU: "mkex A B UU  (s,exA) (t,exB) = ((s,t),UU)"
 apply (simp add: mkex_def)
@@ -191,7 +191,7 @@
 declare composch_simps [simp]
 
 
-subsection {* COMPOSITIONALITY on SCHEDULE Level *}
+subsection \<open>COMPOSITIONALITY on SCHEDULE Level\<close>
 
 subsubsection "Lemmas for ==>"
 
@@ -215,7 +215,7 @@
 lemma lemma_2_1b:
    "filter_act$(ProjA2$xs) =filter_act$xs &
     filter_act$(ProjB2$xs) =filter_act$xs"
-apply (tactic {* pair_induct_tac @{context} "xs" [] 1 *})
+apply (tactic \<open>pair_induct_tac @{context} "xs" [] 1\<close>)
 done
 
 
@@ -230,8 +230,8 @@
 lemma sch_actions_in_AorB: "!s. is_exec_frag (A\<parallel>B) (s,xs)
    --> Forall (%x. x:act (A\<parallel>B)) (filter_act$xs)"
 
-apply (tactic {* pair_induct_tac @{context} "xs" [@{thm is_exec_frag_def}, @{thm Forall_def},
-  @{thm sforall_def}] 1 *})
+apply (tactic \<open>pair_induct_tac @{context} "xs" [@{thm is_exec_frag_def}, @{thm Forall_def},
+  @{thm sforall_def}] 1\<close>)
 (* main case *)
 apply auto
 apply (simp add: trans_of_defs2 actions_asig_comp asig_of_par)
@@ -251,20 +251,20 @@
   Filter (%a. a:act B)$sch << filter_act$exB
   --> filter_act$(snd (mkex A B sch (s,exA) (t,exB))) = sch"
 
-apply (tactic {* Seq_induct_tac @{context} "sch" [@{thm Filter_def}, @{thm Forall_def},
-  @{thm sforall_def}, @{thm mkex_def}] 1 *})
+apply (tactic \<open>Seq_induct_tac @{context} "sch" [@{thm Filter_def}, @{thm Forall_def},
+  @{thm sforall_def}, @{thm mkex_def}] 1\<close>)
 
 (* main case *)
 (* splitting into 4 cases according to a:A, a:B *)
 apply auto
 
 (* Case y:A, y:B *)
-apply (tactic {* Seq_case_simp_tac @{context} "exA" 1 *})
+apply (tactic \<open>Seq_case_simp_tac @{context} "exA" 1\<close>)
 (* Case exA=UU, Case exA=nil*)
 (* These UU and nil cases are the only places where the assumption filter A sch<<f_act exA
    is used! --> to generate a contradiction using  ~a\<leadsto>ss<< UU(nil), using theorems
    Cons_not_less_UU and Cons_not_less_nil  *)
-apply (tactic {* Seq_case_simp_tac @{context} "exB" 1 *})
+apply (tactic \<open>Seq_case_simp_tac @{context} "exB" 1\<close>)
 (* Case exA=a\<leadsto>x, exB=b\<leadsto>y *)
 (* here it is important that Seq_case_simp_tac uses no !full!_simp_tac for the cons case,
    as otherwise mkex_cons_3 would  not be rewritten without use of rotate_tac: then tactic
@@ -272,11 +272,11 @@
 apply simp
 
 (* Case y:A, y~:B *)
-apply (tactic {* Seq_case_simp_tac @{context} "exA" 1 *})
+apply (tactic \<open>Seq_case_simp_tac @{context} "exA" 1\<close>)
 apply simp
 
 (* Case y~:A, y:B *)
-apply (tactic {* Seq_case_simp_tac @{context} "exB" 1 *})
+apply (tactic \<open>Seq_case_simp_tac @{context} "exB" 1\<close>)
 apply simp
 
 (* Case y~:A, y~:B *)
@@ -286,7 +286,7 @@
 
 (* generalizing the proof above to a proof method *)
 
-ML {*
+ML \<open>
 
 local
   val defs = [@{thm Filter_def}, @{thm Forall_def}, @{thm sforall_def}, @{thm mkex_def},
@@ -310,12 +310,12 @@
         ]
 
 end
-*}
+\<close>
 
-method_setup mkex_induct = {*
+method_setup mkex_induct = \<open>
   Scan.lift (Args.name -- Args.name -- Args.name)
     >> (fn ((sch, exA), exB) => fn ctxt => SIMPLE_METHOD' (mkex_induct_tac ctxt sch exA exB))
-*}
+\<close>
 
 
 (*---------------------------------------------------------------------------
@@ -393,7 +393,7 @@
   --------------------------------------------------------------------------- *)
 
 lemma Zip_Map_fst_snd: "Zip$(Map fst$y)$(Map snd$y) = y"
-apply (tactic {* Seq_induct_tac @{context} "y" [] 1 *})
+apply (tactic \<open>Seq_induct_tac @{context} "y" [] 1\<close>)
 done
 
 
@@ -421,8 +421,8 @@
   Filter (%a. a:act B)$sch = filter_act$(snd exB) |]
   ==> Filter_ex (asig_of A) (ProjA (mkex A B sch exA exB)) = exA"
 apply (simp add: ProjA_def Filter_ex_def)
-apply (tactic {* pair_tac @{context} "exA" 1 *})
-apply (tactic {* pair_tac @{context} "exB" 1 *})
+apply (tactic \<open>pair_tac @{context} "exA" 1\<close>)
+apply (tactic \<open>pair_tac @{context} "exB" 1\<close>)
 apply (rule conjI)
 apply (simp (no_asm) add: mkex_def)
 apply (simplesubst trick_against_eq_in_ass)
@@ -462,8 +462,8 @@
   Filter (%a. a:act B)$sch = filter_act$(snd exB) |]
   ==> Filter_ex (asig_of B) (ProjB (mkex A B sch exA exB)) = exB"
 apply (simp add: ProjB_def Filter_ex_def)
-apply (tactic {* pair_tac @{context} "exA" 1 *})
-apply (tactic {* pair_tac @{context} "exB" 1 *})
+apply (tactic \<open>pair_tac @{context} "exA" 1\<close>)
+apply (tactic \<open>pair_tac @{context} "exB" 1\<close>)
 apply (rule conjI)
 apply (simp (no_asm) add: mkex_def)
 apply (simplesubst trick_against_eq_in_ass)
@@ -508,7 +508,7 @@
 apply (simp add: compositionality_ex)
 apply (simp (no_asm) add: Filter_ex_def ProjB_def lemma_2_1a lemma_2_1b)
 apply (simp add: executions_def)
-apply (tactic {* pair_tac @{context} "ex" 1 *})
+apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
 apply (erule conjE)
 apply (simp add: sch_actions_in_AorB)
 
@@ -519,20 +519,20 @@
 apply (rename_tac exA exB)
 apply (rule_tac x = "mkex A B sch exA exB" in bexI)
 (* mkex actions are just the oracle *)
-apply (tactic {* pair_tac @{context} "exA" 1 *})
-apply (tactic {* pair_tac @{context} "exB" 1 *})
+apply (tactic \<open>pair_tac @{context} "exA" 1\<close>)
+apply (tactic \<open>pair_tac @{context} "exB" 1\<close>)
 apply (simp add: Mapfst_mkex_is_sch)
 
 (* mkex is an execution -- use compositionality on ex-level *)
 apply (simp add: compositionality_ex)
 apply (simp add: stutter_mkex_on_A stutter_mkex_on_B filter_mkex_is_exB filter_mkex_is_exA)
-apply (tactic {* pair_tac @{context} "exA" 1 *})
-apply (tactic {* pair_tac @{context} "exB" 1 *})
+apply (tactic \<open>pair_tac @{context} "exA" 1\<close>)
+apply (tactic \<open>pair_tac @{context} "exB" 1\<close>)
 apply (simp add: mkex_actions_in_AorB)
 done
 
 
-subsection {* COMPOSITIONALITY on SCHEDULE Level -- for Modules *}
+subsection \<open>COMPOSITIONALITY on SCHEDULE Level -- for Modules\<close>
 
 lemma compositionality_sch_modules:
   "Scheds (A\<parallel>B) = par_scheds (Scheds A) (Scheds B)"
diff -r 1f2788fb0b8b -r f1599e98c4d0 src/HOL/HOLCF/IOA/meta_theory/CompoTraces.thy
--- a/src/HOL/HOLCF/IOA/meta_theory/CompoTraces.thy	Wed Dec 30 21:56:12 2015 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/CompoTraces.thy	Wed Dec 30 21:57:52 2015 +0100
@@ -2,7 +2,7 @@
     Author:     Olaf Müller
 *) 
 
-section {* Compositionality on Trace level *}
+section \<open>Compositionality on Trace level\<close>
 
 theory CompoTraces
 imports CompoScheds ShortExecutions
@@ -70,7 +70,7 @@
   by (blast intro: finiteR_mksch)
 
 
-declaration {* fn _ => Simplifier.map_ss (Simplifier.set_mksym (K (K NONE))) *}
+declaration \<open>fn _ => Simplifier.map_ss (Simplifier.set_mksym (K (K NONE)))\<close>
 
 
 subsection "mksch rewrite rules"
@@ -165,7 +165,7 @@
 declare compotr_simps [simp]
 
 
-subsection {* COMPOSITIONALITY on TRACE Level *}
+subsection \<open>COMPOSITIONALITY on TRACE Level\<close>
 
 subsubsection "Lemmata for ==>"
 
@@ -201,8 +201,8 @@
   "!!A B. compatible A B ==>  
     ! schA schB. Forall (%x. x:act (A\<parallel>B)) tr  
     --> Forall (%x. x:act (A\<parallel>B)) (mksch A B$tr$schA$schB)"
-apply (tactic {* Seq_induct_tac @{context} "tr"
-  [@{thm Forall_def}, @{thm sforall_def}, @{thm mksch_def}] 1 *})
+apply (tactic \<open>Seq_induct_tac @{context} "tr"
+  [@{thm Forall_def}, @{thm sforall_def}, @{thm mksch_def}] 1\<close>)
 apply auto
 apply (simp add: actions_of_par)
 apply (case_tac "a:act A")
@@ -229,8 +229,8 @@
 lemma ForallBnAmksch [rule_format (no_asm)]: "!!A B. compatible B A  ==>  
     ! schA schB.  (Forall (%x. x:act B & x~:act A) tr  
     --> Forall (%x. x:act B & x~:act A) (mksch A B$tr$schA$schB))"
-apply (tactic {* Seq_induct_tac @{context} "tr"
-  [@{thm Forall_def}, @{thm sforall_def}, @{thm mksch_def}] 1 *})
+apply (tactic \<open>Seq_induct_tac @{context} "tr"
+  [@{thm Forall_def}, @{thm sforall_def}, @{thm mksch_def}] 1\<close>)
 apply auto
 apply (rule Forall_Conc_impl [THEN mp])
 apply (simp add: intA_is_not_actB int_is_act)
@@ -239,8 +239,8 @@
 lemma ForallAnBmksch [rule_format (no_asm)]: "!!A B. compatible A B ==>  
     ! schA schB.  (Forall (%x. x:act A & x~:act B) tr  
     --> Forall (%x. x:act A & x~:act B) (mksch A B$tr$schA$schB))"
-apply (tactic {* Seq_induct_tac @{context} "tr"
-  [@{thm Forall_def}, @{thm sforall_def}, @{thm mksch_def}] 1 *})
+apply (tactic \<open>Seq_induct_tac @{context} "tr"
+  [@{thm Forall_def}, @{thm sforall_def}, @{thm mksch_def}] 1\<close>)
 apply auto
 apply (rule Forall_Conc_impl [THEN mp])
 apply (simp add: intA_is_not_actB int_is_act)
@@ -414,8 +414,8 @@
   Filter (%a. a:act B)$tr << Filter (%a. a:ext B)$schB   
   --> Filter (%a. a:ext (A\<parallel>B))$(mksch A B$tr$schA$schB) = tr"
 
-apply (tactic {* Seq_induct_tac @{context} "tr"
-  [@{thm Forall_def}, @{thm sforall_def}, @{thm mksch_def}] 1 *})
+apply (tactic \<open>Seq_induct_tac @{context} "tr"
+  [@{thm Forall_def}, @{thm sforall_def}, @{thm mksch_def}] 1\<close>)
 (* main case *)
 (* splitting into 4 cases according to a:A, a:B *)
 apply auto
@@ -955,7 +955,7 @@
 
 
 
-subsection {* COMPOSITIONALITY on TRACE Level -- for Modules *}
+subsection \<open>COMPOSITIONALITY on TRACE Level -- for Modules\<close>
 
 lemma compositionality_tr_modules: 
 
@@ -970,7 +970,7 @@
 done
 
 
-declaration {* fn _ => Simplifier.map_ss (Simplifier.set_mksym Simplifier.default_mk_sym) *}
+declaration \<open>fn _ => Simplifier.map_ss (Simplifier.set_mksym Simplifier.default_mk_sym)\<close>
 
 
 end
diff -r 1f2788fb0b8b -r f1599e98c4d0 src/HOL/HOLCF/IOA/meta_theory/Compositionality.thy
--- a/src/HOL/HOLCF/IOA/meta_theory/Compositionality.thy	Wed Dec 30 21:56:12 2015 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/Compositionality.thy	Wed Dec 30 21:57:52 2015 +0100
@@ -2,7 +2,7 @@
     Author:     Olaf Müller
 *)
 
-section {* Compositionality of I/O automata *}
+section \<open>Compositionality of I/O automata\<close>
 theory Compositionality
 imports CompoTraces
 begin
diff -r 1f2788fb0b8b -r f1599e98c4d0 src/HOL/HOLCF/IOA/meta_theory/Deadlock.thy
--- a/src/HOL/HOLCF/IOA/meta_theory/Deadlock.thy	Wed Dec 30 21:56:12 2015 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/Deadlock.thy	Wed Dec 30 21:57:52 2015 +0100
@@ -2,13 +2,13 @@
     Author:     Olaf Müller
 *)
 
-section {* Deadlock freedom of I/O Automata *}
+section \<open>Deadlock freedom of I/O Automata\<close>
 
 theory Deadlock
 imports RefCorrectness CompoScheds
 begin
 
-text {* input actions may always be added to a schedule *}
+text \<open>input actions may always be added to a schedule\<close>
 
 lemma scheds_input_enabled:
   "[| Filter (%x. x:act A)$sch : schedules A; a:inp A; input_enabled A; Finite sch|]  
@@ -17,7 +17,7 @@
 apply auto
 apply (frule inp_is_act)
 apply (simp add: executions_def)
-apply (tactic {* pair_tac @{context} "ex" 1 *})
+apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
 apply (rename_tac s ex)
 apply (subgoal_tac "Finite ex")
 prefer 2
@@ -47,12 +47,12 @@
 apply assumption
 done
 
-text {*
+text \<open>
                Deadlock freedom: component B cannot block an out or int action
                                  of component A in every schedule.
     Needs compositionality on schedule level, input-enabledness, compatibility
                     and distributivity of is_exec_frag over @@
-*}
+\<close>
 
 declare split_if [split del]
 lemma IOA_deadlock_free: "[| a : local A; Finite sch; sch : schedules (A\<parallel>B);  
diff -r 1f2788fb0b8b -r f1599e98c4d0 src/HOL/HOLCF/IOA/meta_theory/IOA.thy
--- a/src/HOL/HOLCF/IOA/meta_theory/IOA.thy	Wed Dec 30 21:56:12 2015 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/IOA.thy	Wed Dec 30 21:57:52 2015 +0100
@@ -2,7 +2,7 @@
     Author:     Olaf Müller
 *)
 
-section {* The theory of I/O automata in HOLCF *}
+section \<open>The theory of I/O automata in HOLCF\<close>
 
 theory IOA
 imports SimCorrectness Compositionality Deadlock
diff -r 1f2788fb0b8b -r f1599e98c4d0 src/HOL/HOLCF/IOA/meta_theory/LiveIOA.thy
--- a/src/HOL/HOLCF/IOA/meta_theory/LiveIOA.thy	Wed Dec 30 21:56:12 2015 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/LiveIOA.thy	Wed Dec 30 21:57:52 2015 +0100
@@ -2,7 +2,7 @@
     Author:     Olaf Müller
 *)
 
-section {* Live I/O automata -- specified by temproal formulas *}
+section \<open>Live I/O automata -- specified by temproal formulas\<close>
 
 theory LiveIOA
 imports TLS
@@ -61,14 +61,14 @@
 apply (rule_tac x = "corresp_ex A f ex" in exI)
 apply auto
   (* Traces coincide, Lemma 1 *)
-  apply (tactic {* pair_tac @{context} "ex" 1 *})
+  apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
   apply (erule lemma_1 [THEN spec, THEN mp])
   apply (simp (no_asm) add: externals_def)
   apply (auto)[1]
   apply (simp add: executions_def reachable.reachable_0)
 
   (* corresp_ex is execution, Lemma 2 *)
-  apply (tactic {* pair_tac @{context} "ex" 1 *})
+  apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
   apply (simp add: executions_def)
   (* start state *)
   apply (rule conjI)
diff -r 1f2788fb0b8b -r f1599e98c4d0 src/HOL/HOLCF/IOA/meta_theory/Pred.thy
--- a/src/HOL/HOLCF/IOA/meta_theory/Pred.thy	Wed Dec 30 21:56:12 2015 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/Pred.thy	Wed Dec 30 21:57:52 2015 +0100
@@ -2,7 +2,7 @@
     Author:     Olaf Müller
 *)
 
-section {* Logical Connectives lifted to predicates *}
+section \<open>Logical Connectives lifted to predicates\<close>
 
 theory Pred
 imports Main
diff -r 1f2788fb0b8b -r f1599e98c4d0 src/HOL/HOLCF/IOA/meta_theory/RefCorrectness.thy
--- a/src/HOL/HOLCF/IOA/meta_theory/RefCorrectness.thy	Wed Dec 30 21:56:12 2015 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/RefCorrectness.thy	Wed Dec 30 21:57:52 2015 +0100
@@ -2,7 +2,7 @@
     Author:     Olaf Müller
 *)
 
-section {* Correctness of Refinement Mappings in HOLCF/IOA *}
+section \<open>Correctness of Refinement Mappings in HOLCF/IOA\<close>
 
 theory RefCorrectness
 imports RefMappings
@@ -180,7 +180,7 @@
          !s. reachable C s & is_exec_frag C (s,xs) -->
              mk_trace C$xs = mk_trace A$(snd (corresp_ex A f (s,xs)))"
 apply (unfold corresp_ex_def)
-apply (tactic {* pair_induct_tac @{context} "xs" [@{thm is_exec_frag_def}] 1 *})
+apply (tactic \<open>pair_induct_tac @{context} "xs" [@{thm is_exec_frag_def}] 1\<close>)
 (* cons case *)
 apply (auto simp add: mk_traceConc)
 apply (frule reachable.reachable_n)
@@ -208,7 +208,7 @@
   --> is_exec_frag A (s,xs @@ ys))"
 
 apply (rule impI)
-apply (tactic {* Seq_Finite_induct_tac @{context} 1 *})
+apply (tactic \<open>Seq_Finite_induct_tac @{context} 1\<close>)
 (* main case *)
 apply (auto simp add: split_paired_all)
 done
@@ -228,7 +228,7 @@
 apply (unfold corresp_ex_def)
 
 apply simp
-apply (tactic {* pair_induct_tac @{context} "xs" [@{thm is_exec_frag_def}] 1 *})
+apply (tactic \<open>pair_induct_tac @{context} "xs" [@{thm is_exec_frag_def}] 1\<close>)
 (* main case *)
 apply auto
 apply (rule_tac t = "f x2" in lemma_2_1)
@@ -271,13 +271,13 @@
   apply (rule_tac x = "corresp_ex A f ex" in bexI)
 
   (* Traces coincide, Lemma 1 *)
-  apply (tactic {* pair_tac @{context} "ex" 1 *})
+  apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
   apply (erule lemma_1 [THEN spec, THEN mp])
   apply assumption+
   apply (simp add: executions_def reachable.reachable_0)
 
   (* corresp_ex is execution, Lemma 2 *)
-  apply (tactic {* pair_tac @{context} "ex" 1 *})
+  apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
   apply (simp add: executions_def)
   (* start state *)
   apply (rule conjI)
@@ -322,13 +322,13 @@
 apply auto
 
   (* Traces coincide, Lemma 1 *)
-  apply (tactic {* pair_tac @{context} "ex" 1 *})
+  apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
   apply (erule lemma_1 [THEN spec, THEN mp])
   apply assumption+
   apply (simp add: executions_def reachable.reachable_0)
 
   (* corresp_ex is execution, Lemma 2 *)
-  apply (tactic {* pair_tac @{context} "ex" 1 *})
+  apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
   apply (simp add: executions_def)
   (* start state *)
   apply (rule conjI)
@@ -349,14 +349,14 @@
 apply auto
 
   (* Traces coincide, Lemma 1 *)
-  apply (tactic {* pair_tac @{context} "ex" 1 *})
+  apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
   apply (erule lemma_1 [THEN spec, THEN mp])
   apply (simp (no_asm) add: externals_def)
   apply (auto)[1]
   apply (simp add: executions_def reachable.reachable_0)
 
   (* corresp_ex is execution, Lemma 2 *)
-  apply (tactic {* pair_tac @{context} "ex" 1 *})
+  apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
   apply (simp add: executions_def)
   (* start state *)
   apply (rule conjI)
diff -r 1f2788fb0b8b -r f1599e98c4d0 src/HOL/HOLCF/IOA/meta_theory/RefMappings.thy
--- a/src/HOL/HOLCF/IOA/meta_theory/RefMappings.thy	Wed Dec 30 21:56:12 2015 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/RefMappings.thy	Wed Dec 30 21:57:52 2015 +0100
@@ -2,7 +2,7 @@
     Author:     Olaf Müller
 *)
 
-section {* Refinement Mappings in HOLCF/IOA *}
+section \<open>Refinement Mappings in HOLCF/IOA\<close>
 
 theory RefMappings
 imports Traces
diff -r 1f2788fb0b8b -r f1599e98c4d0 src/HOL/HOLCF/IOA/meta_theory/Seq.thy
--- a/src/HOL/HOLCF/IOA/meta_theory/Seq.thy	Wed Dec 30 21:56:12 2015 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/Seq.thy	Wed Dec 30 21:57:52 2015 +0100
@@ -2,7 +2,7 @@
     Author:     Olaf Müller
 *)
 
-section {* Partial, Finite and Infinite Sequences (lazy lists), modeled as domain *}
+section \<open>Partial, Finite and Infinite Sequences (lazy lists), modeled as domain\<close>
 
 theory Seq
 imports "../../HOLCF"
@@ -51,9 +51,9 @@
   "Infinite x == ~(seq_finite x)"
 
 
-subsection {* recursive equations of operators *}
+subsection \<open>recursive equations of operators\<close>
 
-subsubsection {* smap *}
+subsubsection \<open>smap\<close>
 
 fixrec
   smap :: "('a -> 'b) -> 'a seq -> 'b seq"
@@ -64,7 +64,7 @@
 lemma smap_UU [simp]: "smap$f$UU=UU"
 by fixrec_simp
 
-subsubsection {* sfilter *}
+subsubsection \<open>sfilter\<close>
 
 fixrec
    sfilter :: "('a -> tr) -> 'a seq -> 'a seq"
@@ -77,7 +77,7 @@
 lemma sfilter_UU [simp]: "sfilter$P$UU=UU"
 by fixrec_simp
 
-subsubsection {* sforall2 *}
+subsubsection \<open>sforall2\<close>
 
 fixrec
   sforall2 :: "('a -> tr) -> 'a seq -> tr"
@@ -92,7 +92,7 @@
 definition
   sforall_def: "sforall P t == (sforall2$P$t ~=FF)"
 
-subsubsection {* stakewhile *}
+subsubsection \<open>stakewhile\<close>
 
 fixrec
   stakewhile :: "('a -> tr)  -> 'a seq -> 'a seq"
@@ -105,7 +105,7 @@
 lemma stakewhile_UU [simp]: "stakewhile$P$UU=UU"
 by fixrec_simp
 
-subsubsection {* sdropwhile *}
+subsubsection \<open>sdropwhile\<close>
 
 fixrec
   sdropwhile :: "('a -> tr) -> 'a seq -> 'a seq"
@@ -118,7 +118,7 @@
 lemma sdropwhile_UU [simp]: "sdropwhile$P$UU=UU"
 by fixrec_simp
 
-subsubsection {* slast *}
+subsubsection \<open>slast\<close>
 
 fixrec
   slast :: "'a seq -> 'a"
@@ -130,7 +130,7 @@
 lemma slast_UU [simp]: "slast$UU=UU"
 by fixrec_simp
 
-subsubsection {* sconc *}
+subsubsection \<open>sconc\<close>
 
 fixrec
   sconc :: "'a seq -> 'a seq -> 'a seq"
@@ -153,7 +153,7 @@
 
 declare sconc_cons' [simp del]
 
-subsubsection {* sflat *}
+subsubsection \<open>sflat\<close>
 
 fixrec
   sflat :: "('a seq) seq -> 'a seq"
@@ -169,7 +169,7 @@
 
 declare sflat_cons' [simp del]
 
-subsubsection {* szip *}
+subsubsection \<open>szip\<close>
 
 fixrec
   szip :: "'a seq -> 'b seq -> ('a*'b) seq"
diff -r 1f2788fb0b8b -r f1599e98c4d0 src/HOL/HOLCF/IOA/meta_theory/Sequence.thy
--- a/src/HOL/HOLCF/IOA/meta_theory/Sequence.thy	Wed Dec 30 21:56:12 2015 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/Sequence.thy	Wed Dec 30 21:57:52 2015 +0100
@@ -93,7 +93,7 @@
 by (simp add: Map_def Consq_def flift2_def)
 
 
-subsubsection {* Filter *}
+subsubsection \<open>Filter\<close>
 
 lemma Filter_UU: "Filter P$UU =UU"
 by (simp add: Filter_def)
@@ -106,7 +106,7 @@
 by (simp add: Filter_def Consq_def flift2_def If_and_if)
 
 
-subsubsection {* Forall *}
+subsubsection \<open>Forall\<close>
 
 lemma Forall_UU: "Forall P UU"
 by (simp add: Forall_def sforall_def)
@@ -118,13 +118,13 @@
 by (simp add: Forall_def sforall_def Consq_def flift2_def)
 
 
-subsubsection {* Conc *}
+subsubsection \<open>Conc\<close>
 
 lemma Conc_cons: "(x\<leadsto>xs) @@ y = x\<leadsto>(xs @@y)"
 by (simp add: Consq_def)
 
 
-subsubsection {* Takewhile *}
+subsubsection \<open>Takewhile\<close>
 
 lemma Takewhile_UU: "Takewhile P$UU =UU"
 by (simp add: Takewhile_def)
@@ -137,7 +137,7 @@
 by (simp add: Takewhile_def Consq_def flift2_def If_and_if)
 
 
-subsubsection {* DropWhile *}
+subsubsection \<open>DropWhile\<close>
 
 lemma Dropwhile_UU: "Dropwhile P$UU =UU"
 by (simp add: Dropwhile_def)
@@ -150,7 +150,7 @@
 by (simp add: Dropwhile_def Consq_def flift2_def If_and_if)
 
 
-subsubsection {* Last *}
+subsubsection \<open>Last\<close>
 
 lemma Last_UU: "Last$UU =UU"
 by (simp add: Last_def)
@@ -165,7 +165,7 @@
 done
 
 
-subsubsection {* Flat *}
+subsubsection \<open>Flat\<close>
 
 lemma Flat_UU: "Flat$UU =UU"
 by (simp add: Flat_def)
@@ -177,7 +177,7 @@
 by (simp add: Flat_def Consq_def)
 
 
-subsubsection {* Zip *}
+subsubsection \<open>Zip\<close>
 
 lemma Zip_unfold:
 "Zip = (LAM t1 t2. case t1 of
@@ -1075,7 +1075,7 @@
 done
 
 
-ML {*
+ML \<open>
 
 fun Seq_case_tac ctxt s i =
   Rule_Insts.res_inst_tac ctxt [((("x", 0), Position.none), s)] [] @{thm Seq_cases} i
@@ -1109,6 +1109,6 @@
   THEN (REPEAT_DETERM (CHANGED (simp_tac ctxt (i+1))))
   THEN simp_tac (ctxt addsimps rws) i;
 
-*}
+\<close>
 
 end
diff -r 1f2788fb0b8b -r f1599e98c4d0 src/HOL/HOLCF/IOA/meta_theory/ShortExecutions.thy
--- a/src/HOL/HOLCF/IOA/meta_theory/ShortExecutions.thy	Wed Dec 30 21:56:12 2015 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/ShortExecutions.thy	Wed Dec 30 21:57:52 2015 +0100
@@ -6,12 +6,12 @@
 imports Traces
 begin
 
-text {*
-  Some properties about @{text "Cut ex"}, defined as follows:
+text \<open>
+  Some properties about \<open>Cut ex\<close>, defined as follows:
 
-  For every execution ex there is another shorter execution @{text "Cut ex"}
+  For every execution ex there is another shorter execution \<open>Cut ex\<close>
   that has the same trace as ex, but its schedule ends with an external action.
-*}
+\<close>
 
 definition
   oraclebuild :: "('a => bool) => 'a Seq -> 'a Seq -> 'a Seq" where
@@ -47,12 +47,12 @@
   LastActExtsmall2: "[| Finite sch1; LastActExtsch A (sch1 @@ sch2) |] ==> LastActExtsch A sch2"
 
 
-ML {*
+ML \<open>
 fun thin_tac' ctxt j =
   rotate_tac (j - 1) THEN'
   eresolve_tac ctxt [thin_rl] THEN'
   rotate_tac (~ (j - 1))
-*}
+\<close>
 
 
 subsection "oraclebuild rewrite rules"
@@ -225,7 +225,7 @@
 apply auto
 apply (rule_tac x = "filter_act$ (Cut (%a. fst a:ext A) (snd ex))" in exI)
 apply (simp add: executions_def)
-apply (tactic {* pair_tac @{context} "ex" 1 *})
+apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
 apply auto
 apply (rule_tac x = " (x1,Cut (%a. fst a:ext A) x2) " in exI)
 apply (simp (no_asm_simp))
diff -r 1f2788fb0b8b -r f1599e98c4d0 src/HOL/HOLCF/IOA/meta_theory/SimCorrectness.thy
--- a/src/HOL/HOLCF/IOA/meta_theory/SimCorrectness.thy	Wed Dec 30 21:56:12 2015 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/SimCorrectness.thy	Wed Dec 30 21:57:52 2015 +0100
@@ -2,7 +2,7 @@
     Author:     Olaf Müller
 *)
 
-section {* Correctness of Simulations in HOLCF/IOA *}
+section \<open>Correctness of Simulations in HOLCF/IOA\<close>
 
 theory SimCorrectness
 imports Simulations
@@ -156,7 +156,7 @@
 done
 
 
-subsection {* TRACE INCLUSION Part 1: Traces coincide *}
+subsection \<open>TRACE INCLUSION Part 1: Traces coincide\<close>
 
 subsubsection "Lemmata for <=="
 
@@ -170,7 +170,7 @@
          !s s'. reachable C s & is_exec_frag C (s,ex) & (s,s'): R -->
              mk_trace C$ex = mk_trace A$((corresp_ex_simC A R$ex) s')"
 
-apply (tactic {* pair_induct_tac @{context} "ex" [@{thm is_exec_frag_def}] 1 *})
+apply (tactic \<open>pair_induct_tac @{context} "ex" [@{thm is_exec_frag_def}] 1\<close>)
 (* cons case *)
 apply auto
 apply (rename_tac ex a t s s')
@@ -195,7 +195,7 @@
   !s s'. reachable C s & is_exec_frag C (s,ex) & (s,s'):R
   --> is_exec_frag A (s',(corresp_ex_simC A R$ex) s')"
 
-apply (tactic {* pair_induct_tac @{context} "ex" [@{thm is_exec_frag_def}] 1 *})
+apply (tactic \<open>pair_induct_tac @{context} "ex" [@{thm is_exec_frag_def}] 1\<close>)
 (* main case *)
 apply auto
 apply (rename_tac ex a t s s')
@@ -265,7 +265,7 @@
   apply (rule_tac x = "corresp_ex_sim A R ex" in bexI)
 
   (* Traces coincide, Lemma 1 *)
-  apply (tactic {* pair_tac @{context} "ex" 1 *})
+  apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
   apply (rename_tac s ex)
   apply (simp (no_asm) add: corresp_ex_sim_def)
   apply (rule_tac s = "s" in traces_coincide_sim)
@@ -273,7 +273,7 @@
   apply (simp add: executions_def reachable.reachable_0 sim_starts1)
 
   (* corresp_ex_sim is execution, Lemma 2 *)
-  apply (tactic {* pair_tac @{context} "ex" 1 *})
+  apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
   apply (simp add: executions_def)
   apply (rename_tac s ex)
 
diff -r 1f2788fb0b8b -r f1599e98c4d0 src/HOL/HOLCF/IOA/meta_theory/Simulations.thy
--- a/src/HOL/HOLCF/IOA/meta_theory/Simulations.thy	Wed Dec 30 21:56:12 2015 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/Simulations.thy	Wed Dec 30 21:57:52 2015 +0100
@@ -2,7 +2,7 @@
     Author:     Olaf Müller
 *)
 
-section {* Simulations in HOLCF/IOA *}
+section \<open>Simulations in HOLCF/IOA\<close>
 
 theory Simulations
 imports RefCorrectness
diff -r 1f2788fb0b8b -r f1599e98c4d0 src/HOL/HOLCF/IOA/meta_theory/TL.thy
--- a/src/HOL/HOLCF/IOA/meta_theory/TL.thy	Wed Dec 30 21:56:12 2015 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/TL.thy	Wed Dec 30 21:57:52 2015 +0100
@@ -2,7 +2,7 @@
     Author:     Olaf Müller
 *)
 
-section {* A General Temporal Logic *}
+section \<open>A General Temporal Logic\<close>
 
 theory TL
 imports Pred Sequence
@@ -147,7 +147,7 @@
 "s~=UU & s~=nil --> tsuffix s2 (TL$s) --> tsuffix s2 s"
 apply (unfold tsuffix_def suffix_def)
 apply auto
-apply (tactic {* Seq_case_simp_tac @{context} "s" 1 *})
+apply (tactic \<open>Seq_case_simp_tac @{context} "s" 1\<close>)
 apply (rule_tac x = "a\<leadsto>s1" in exI)
 apply auto
 done
diff -r 1f2788fb0b8b -r f1599e98c4d0 src/HOL/HOLCF/IOA/meta_theory/TLS.thy
--- a/src/HOL/HOLCF/IOA/meta_theory/TLS.thy	Wed Dec 30 21:56:12 2015 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/TLS.thy	Wed Dec 30 21:57:52 2015 +0100
@@ -2,7 +2,7 @@
     Author:     Olaf Müller
 *)
 
-section {* Temporal Logic of Steps -- tailored for I/O automata *}
+section \<open>Temporal Logic of Steps -- tailored for I/O automata\<close>
 
 theory TLS
 imports IOA TL
@@ -92,10 +92,10 @@
 
 lemmas [simp del] = HOL.ex_simps HOL.all_simps split_paired_Ex
 
-setup {* map_theory_claset (fn ctxt => ctxt delSWrapper "split_all_tac") *}
+setup \<open>map_theory_claset (fn ctxt => ctxt delSWrapper "split_all_tac")\<close>
 
 
-subsection {* ex2seqC *}
+subsection \<open>ex2seqC\<close>
 
 lemma ex2seqC_unfold: "ex2seqC  = (LAM ex. (%s. case ex of  
        nil =>  (s,None,s)\<leadsto>nil    
@@ -151,13 +151,13 @@
 
 
 lemma ex2seq_nUUnnil: "ex2seq exec ~= UU & ex2seq exec ~= nil"
-apply (tactic {* pair_tac @{context} "exec" 1 *})
-apply (tactic {* Seq_case_simp_tac @{context} "x2" 1 *})
-apply (tactic {* pair_tac @{context} "a" 1 *})
+apply (tactic \<open>pair_tac @{context} "exec" 1\<close>)
+apply (tactic \<open>Seq_case_simp_tac @{context} "x2" 1\<close>)
+apply (tactic \<open>pair_tac @{context} "a" 1\<close>)
 done
 
 
-subsection {* Interface TL -- TLS *}
+subsection \<open>Interface TL -- TLS\<close>
 
 (* uses the fact that in executions states overlap, which is lost in 
    after the translation via ex2seq !! *)
@@ -172,31 +172,31 @@
 apply (simp split add: split_if)
 (* TL = UU *)
 apply (rule conjI)
-apply (tactic {* pair_tac @{context} "ex" 1 *})
-apply (tactic {* Seq_case_simp_tac @{context} "x2" 1 *})
-apply (tactic {* pair_tac @{context} "a" 1 *})
-apply (tactic {* Seq_case_simp_tac @{context} "s" 1 *})
-apply (tactic {* pair_tac @{context} "a" 1 *})
+apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
+apply (tactic \<open>Seq_case_simp_tac @{context} "x2" 1\<close>)
+apply (tactic \<open>pair_tac @{context} "a" 1\<close>)
+apply (tactic \<open>Seq_case_simp_tac @{context} "s" 1\<close>)
+apply (tactic \<open>pair_tac @{context} "a" 1\<close>)
 (* TL = nil *)
 apply (rule conjI)
-apply (tactic {* pair_tac @{context} "ex" 1 *})
-apply (tactic {* Seq_case_tac @{context} "x2" 1 *})
+apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
+apply (tactic \<open>Seq_case_tac @{context} "x2" 1\<close>)
 apply (simp add: unlift_def)
 apply fast
 apply (simp add: unlift_def)
 apply fast
 apply (simp add: unlift_def)
-apply (tactic {* pair_tac @{context} "a" 1 *})
-apply (tactic {* Seq_case_simp_tac @{context} "s" 1 *})
-apply (tactic {* pair_tac @{context} "a" 1 *})
+apply (tactic \<open>pair_tac @{context} "a" 1\<close>)
+apply (tactic \<open>Seq_case_simp_tac @{context} "s" 1\<close>)
+apply (tactic \<open>pair_tac @{context} "a" 1\<close>)
 (* TL =cons *)
 apply (simp add: unlift_def)
 
-apply (tactic {* pair_tac @{context} "ex" 1 *})
-apply (tactic {* Seq_case_simp_tac @{context} "x2" 1 *})
-apply (tactic {* pair_tac @{context} "a" 1 *})
-apply (tactic {* Seq_case_simp_tac @{context} "s" 1 *})
-apply (tactic {* pair_tac @{context} "a" 1 *})
+apply (tactic \<open>pair_tac @{context} "ex" 1\<close>)
+apply (tactic \<open>Seq_case_simp_tac @{context} "x2" 1\<close>)
+apply (tactic \<open>pair_tac @{context} "a" 1\<close>)
+apply (tactic \<open>Seq_case_simp_tac @{context} "s" 1\<close>)
+apply (tactic \<open>pair_tac @{context} "a" 1\<close>)
 done
 
 end
diff -r 1f2788fb0b8b -r f1599e98c4d0 src/HOL/HOLCF/IOA/meta_theory/Traces.thy
--- a/src/HOL/HOLCF/IOA/meta_theory/Traces.thy	Wed Dec 30 21:56:12 2015 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/Traces.thy	Wed Dec 30 21:57:52 2015 +0100
@@ -2,7 +2,7 @@
     Author:     Olaf Müller
 *)
 
-section {* Executions and Traces of I/O automata in HOLCF *}
+section \<open>Executions and Traces of I/O automata in HOLCF\<close>
 
 theory Traces
 imports Sequence Automata
@@ -203,7 +203,7 @@
 
 lemmas [simp del] = HOL.ex_simps HOL.all_simps split_paired_Ex
 declare Let_def [simp]
-setup {* map_theory_claset (fn ctxt => ctxt delSWrapper "split_all_tac") *}
+setup \<open>map_theory_claset (fn ctxt => ctxt delSWrapper "split_all_tac")\<close>
 
 lemmas exec_rws = executions_def is_exec_frag_def
 
@@ -367,8 +367,8 @@
 lemma execfrag_in_sig: 
   "!! A. is_trans_of A ==>  
   ! s. is_exec_frag A (s,xs) --> Forall (%a. a:act A) (filter_act$xs)"
-apply (tactic {* pair_induct_tac @{context} "xs" [@{thm is_exec_frag_def},
-  @{thm Forall_def}, @{thm sforall_def}] 1 *})
+apply (tactic \<open>pair_induct_tac @{context} "xs" [@{thm is_exec_frag_def},
+  @{thm Forall_def}, @{thm sforall_def}] 1\<close>)
 (* main case *)
 apply (auto simp add: is_trans_of_def)
 done
@@ -377,7 +377,7 @@
   "!! A.[|  is_trans_of A; x:executions A |] ==>  
   Forall (%a. a:act A) (filter_act$(snd x))"
 apply (simp add: executions_def)
-apply (tactic {* pair_tac @{context} "x" 1 *})
+apply (tactic \<open>pair_tac @{context} "x" 1\<close>)
 apply (rule execfrag_in_sig [THEN spec, THEN mp])
 apply auto
 done
@@ -394,10 +394,10 @@
 
 (* only admissible in y, not if done in x !! *)
 lemma execfrag_prefixclosed: "!x s. is_exec_frag A (s,x) & y<<x  --> is_exec_frag A (s,y)"
-apply (tactic {* pair_induct_tac @{context} "y" [@{thm is_exec_frag_def}] 1 *})
+apply (tactic \<open>pair_induct_tac @{context} "y" [@{thm is_exec_frag_def}] 1\<close>)
 apply (intro strip)
-apply (tactic {* Seq_case_simp_tac @{context} "x" 1 *})
-apply (tactic {* pair_tac @{context} "a" 1 *})
+apply (tactic \<open>Seq_case_simp_tac @{context} "x" 1\<close>)
+apply (tactic \<open>pair_tac @{context} "a" 1\<close>)
 apply auto
 done
 
@@ -409,10 +409,10 @@
 
 lemma exec_prefix2closed [rule_format]:
   "! y s. is_exec_frag A (s,x@@y) --> is_exec_frag A (s,x)"
-apply (tactic {* pair_induct_tac @{context} "x" [@{thm is_exec_frag_def}] 1 *})
+apply (tactic \<open>pair_induct_tac @{context} "x" [@{thm is_exec_frag_def}] 1\<close>)
 apply (intro strip)
-apply (tactic {* Seq_case_simp_tac @{context} "s" 1 *})
-apply (tactic {* pair_tac @{context} "a" 1 *})
+apply (tactic \<open>Seq_case_simp_tac @{context} "s" 1\<close>)
+apply (tactic \<open>pair_tac @{context} "a" 1\<close>)
 apply auto
 done