# HG changeset patch
# User wenzelm
# Date 1464169858 -7200
# Node ID f1ecba0272f9bb6a2924276431e3bc68307d7176
# Parent  703edebd1d925381219bcf190342ed066c733a24
isabelle update_cartouches -c -t;

diff -r 703edebd1d92 -r f1ecba0272f9 src/HOL/UNITY/Comp.thy
--- a/src/HOL/UNITY/Comp.thy	Wed May 25 11:49:40 2016 +0200
+++ b/src/HOL/UNITY/Comp.thy	Wed May 25 11:50:58 2016 +0200
@@ -8,7 +8,7 @@
 Technical Report 2000-003, University of Florida, 2000.
 *)
 
-section{*Composition: Basic Primitives*}
+section\<open>Composition: Basic Primitives\<close>
 
 theory Comp
 imports Union
@@ -42,7 +42,7 @@
   where "funPair f g == %x. (f x, g x)"
 
 
-subsection{*The component relation*}
+subsection\<open>The component relation\<close>
 lemma componentI: "H \<le> F | H \<le> G ==> H \<le> (F\<squnion>G)"
 apply (unfold component_def, auto)
 apply (rule_tac x = "G\<squnion>Ga" in exI)
@@ -115,7 +115,7 @@
 lemmas program_less_le = strict_component_def
 
 
-subsection{*The preserves property*}
+subsection\<open>The preserves property\<close>
 
 lemma preservesI: "(!!z. F \<in> stable {s. v s = z}) ==> F \<in> preserves v"
 by (unfold preserves_def, blast)
diff -r 703edebd1d92 -r f1ecba0272f9 src/HOL/UNITY/Comp/Alloc.thy
--- a/src/HOL/UNITY/Comp/Alloc.thy	Wed May 25 11:49:40 2016 +0200
+++ b/src/HOL/UNITY/Comp/Alloc.thy	Wed May 25 11:50:58 2016 +0200
@@ -9,55 +9,55 @@
 imports AllocBase "../PPROD"
 begin
 
-subsection{*State definitions.  OUTPUT variables are locals*}
+subsection\<open>State definitions.  OUTPUT variables are locals\<close>
 
 record clientState =
-  giv :: "nat list"   --{*client's INPUT history:  tokens GRANTED*}
-  ask :: "nat list"   --{*client's OUTPUT history: tokens REQUESTED*}
-  rel :: "nat list"   --{*client's OUTPUT history: tokens RELEASED*}
+  giv :: "nat list"   \<comment>\<open>client's INPUT history:  tokens GRANTED\<close>
+  ask :: "nat list"   \<comment>\<open>client's OUTPUT history: tokens REQUESTED\<close>
+  rel :: "nat list"   \<comment>\<open>client's OUTPUT history: tokens RELEASED\<close>
 
 record 'a clientState_d =
   clientState +
-  dummy :: 'a       --{*dummy field for new variables*}
+  dummy :: 'a       \<comment>\<open>dummy field for new variables\<close>
 
 definition
-  --{*DUPLICATED FROM Client.thy, but with "tok" removed*}
-  --{*Maybe want a special theory section to declare such maps*}
+  \<comment>\<open>DUPLICATED FROM Client.thy, but with "tok" removed\<close>
+  \<comment>\<open>Maybe want a special theory section to declare such maps\<close>
   non_dummy :: "'a clientState_d => clientState"
   where "non_dummy s = (|giv = giv s, ask = ask s, rel = rel s|)"
 
 definition
-  --{*Renaming map to put a Client into the standard form*}
+  \<comment>\<open>Renaming map to put a Client into the standard form\<close>
   client_map :: "'a clientState_d => clientState*'a"
   where "client_map = funPair non_dummy dummy"
 
 
 record allocState =
-  allocGiv :: "nat => nat list"   --{*OUTPUT history: source of "giv" for i*}
-  allocAsk :: "nat => nat list"   --{*INPUT: allocator's copy of "ask" for i*}
-  allocRel :: "nat => nat list"   --{*INPUT: allocator's copy of "rel" for i*}
+  allocGiv :: "nat => nat list"   \<comment>\<open>OUTPUT history: source of "giv" for i\<close>
+  allocAsk :: "nat => nat list"   \<comment>\<open>INPUT: allocator's copy of "ask" for i\<close>
+  allocRel :: "nat => nat list"   \<comment>\<open>INPUT: allocator's copy of "rel" for i\<close>
 
 record 'a allocState_d =
   allocState +
-  dummy    :: 'a                --{*dummy field for new variables*}
+  dummy    :: 'a                \<comment>\<open>dummy field for new variables\<close>
 
 record 'a systemState =
   allocState +
-  client :: "nat => clientState"  --{*states of all clients*}
-  dummy  :: 'a                    --{*dummy field for new variables*}
+  client :: "nat => clientState"  \<comment>\<open>states of all clients\<close>
+  dummy  :: 'a                    \<comment>\<open>dummy field for new variables\<close>
 
 
---{** Resource allocation system specification **}
+\<comment>\<open>* Resource allocation system specification *\<close>
 
 definition
-  --{*spec (1)*}
+  \<comment>\<open>spec (1)\<close>
   system_safety :: "'a systemState program set"
   where "system_safety =
      Always {s. (\<Sum>i \<in> lessThan Nclients. (tokens o giv o sub i o client)s)
      \<le> NbT + (\<Sum>i \<in> lessThan Nclients. (tokens o rel o sub i o client)s)}"
 
 definition
-  --{*spec (2)*}
+  \<comment>\<open>spec (2)\<close>
   system_progress :: "'a systemState program set"
   where "system_progress = (INT i : lessThan Nclients.
                         INT h.
@@ -68,20 +68,20 @@
   system_spec :: "'a systemState program set"
   where "system_spec = system_safety Int system_progress"
 
---{** Client specification (required) ***}
+\<comment>\<open>* Client specification (required) **\<close>
 
 definition
-  --{*spec (3)*}
+  \<comment>\<open>spec (3)\<close>
   client_increasing :: "'a clientState_d program set"
   where "client_increasing = UNIV guarantees  Increasing ask Int Increasing rel"
 
 definition
-  --{*spec (4)*}
+  \<comment>\<open>spec (4)\<close>
   client_bounded :: "'a clientState_d program set"
   where "client_bounded = UNIV guarantees  Always {s. ALL elt : set (ask s). elt \<le> NbT}"
 
 definition
-  --{*spec (5)*}
+  \<comment>\<open>spec (5)\<close>
   client_progress :: "'a clientState_d program set"
   where "client_progress =
          Increasing giv  guarantees
@@ -89,12 +89,12 @@
                  LeadsTo {s. tokens h \<le> (tokens o rel) s})"
 
 definition
-  --{*spec: preserves part*}
+  \<comment>\<open>spec: preserves part\<close>
   client_preserves :: "'a clientState_d program set"
   where "client_preserves = preserves giv Int preserves clientState_d.dummy"
 
 definition
-  --{*environmental constraints*}
+  \<comment>\<open>environmental constraints\<close>
   client_allowed_acts :: "'a clientState_d program set"
   where "client_allowed_acts =
        {F. AllowedActs F =
@@ -105,17 +105,17 @@
   where "client_spec = client_increasing Int client_bounded Int client_progress
                     Int client_allowed_acts Int client_preserves"
 
---{** Allocator specification (required) **}
+\<comment>\<open>* Allocator specification (required) *\<close>
 
 definition
-  --{*spec (6)*}
+  \<comment>\<open>spec (6)\<close>
   alloc_increasing :: "'a allocState_d program set"
   where "alloc_increasing =
          UNIV  guarantees
          (INT i : lessThan Nclients. Increasing (sub i o allocGiv))"
 
 definition
-  --{*spec (7)*}
+  \<comment>\<open>spec (7)\<close>
   alloc_safety :: "'a allocState_d program set"
   where "alloc_safety =
          (INT i : lessThan Nclients. Increasing (sub i o allocRel))
@@ -124,7 +124,7 @@
          \<le> NbT + (\<Sum>i \<in> lessThan Nclients. (tokens o sub i o allocRel)s)}"
 
 definition
-  --{*spec (8)*}
+  \<comment>\<open>spec (8)\<close>
   alloc_progress :: "'a allocState_d program set"
   where "alloc_progress =
          (INT i : lessThan Nclients. Increasing (sub i o allocAsk) Int
@@ -151,13 +151,13 @@
     looked at.*)
 
 definition
-  --{*spec: preserves part*}
+  \<comment>\<open>spec: preserves part\<close>
   alloc_preserves :: "'a allocState_d program set"
   where "alloc_preserves = preserves allocRel Int preserves allocAsk Int
                         preserves allocState_d.dummy"
 
 definition
-  --{*environmental constraints*}
+  \<comment>\<open>environmental constraints\<close>
   alloc_allowed_acts :: "'a allocState_d program set"
   where "alloc_allowed_acts =
        {F. AllowedActs F =
@@ -168,17 +168,17 @@
   where "alloc_spec = alloc_increasing Int alloc_safety Int alloc_progress Int
                    alloc_allowed_acts Int alloc_preserves"
 
---{** Network specification **}
+\<comment>\<open>* Network specification *\<close>
 
 definition
-  --{*spec (9.1)*}
+  \<comment>\<open>spec (9.1)\<close>
   network_ask :: "'a systemState program set"
   where "network_ask = (INT i : lessThan Nclients.
                         Increasing (ask o sub i o client)  guarantees
                         ((sub i o allocAsk) Fols (ask o sub i o client)))"
 
 definition
-  --{*spec (9.2)*}
+  \<comment>\<open>spec (9.2)\<close>
   network_giv :: "'a systemState program set"
   where "network_giv = (INT i : lessThan Nclients.
                         Increasing (sub i o allocGiv)
@@ -186,7 +186,7 @@
                         ((giv o sub i o client) Fols (sub i o allocGiv)))"
 
 definition
-  --{*spec (9.3)*}
+  \<comment>\<open>spec (9.3)\<close>
   network_rel :: "'a systemState program set"
   where "network_rel = (INT i : lessThan Nclients.
                         Increasing (rel o sub i o client)
@@ -194,7 +194,7 @@
                         ((sub i o allocRel) Fols (rel o sub i o client)))"
 
 definition
-  --{*spec: preserves part*}
+  \<comment>\<open>spec: preserves part\<close>
   network_preserves :: "'a systemState program set"
   where "network_preserves =
        preserves allocGiv  Int
@@ -202,7 +202,7 @@
                                    preserves (ask o sub i o client))"
 
 definition
-  --{*environmental constraints*}
+  \<comment>\<open>environmental constraints\<close>
   network_allowed_acts :: "'a systemState program set"
   where "network_allowed_acts =
        {F. AllowedActs F =
@@ -218,7 +218,7 @@
                      network_preserves"
 
 
---{** State mappings **}
+\<comment>\<open>* State mappings *\<close>
 definition
   sysOfAlloc :: "((nat => clientState) * 'a) allocState_d => 'a systemState"
   where "sysOfAlloc = (%s. let (cl,xtr) = allocState_d.dummy s
@@ -300,7 +300,7 @@
   bij_is_inj [THEN image_Int]
   bij_image_Collect_eq
 
-ML {*
+ML \<open>
 (*Splits up conjunctions & intersections: like CONJUNCTS in the HOL system*)
 fun list_of_Int th =
     (list_of_Int (th RS conjunct1) @ list_of_Int (th RS conjunct2))
@@ -308,11 +308,11 @@
     handle THM _ => (list_of_Int (th RS @{thm INT_D}))
     handle THM _ => (list_of_Int (th RS bspec))
     handle THM _ => [th];
-*}
+\<close>
 
 lemmas lessThanBspec = lessThan_iff [THEN iffD2, THEN [2] bspec]
 
-attribute_setup normalized = {*
+attribute_setup normalized = \<open>
 let
   fun normalized th =
     normalized (th RS spec
@@ -323,10 +323,10 @@
 in
   Scan.succeed (Thm.rule_attribute [] (K normalized))
 end
-*}
+\<close>
 
 (*** bijectivity of sysOfAlloc [MUST BE AUTOMATED] ***)
-ML {*
+ML \<open>
 fun record_auto_tac ctxt =
   let val ctxt' =
     ctxt addSWrapper Record.split_wrapper
@@ -336,9 +336,9 @@
         @{thm o_apply}, @{thm Let_def}]
   in auto_tac ctxt' end;
 
-*}
+\<close>
 
-method_setup record_auto = {* Scan.succeed (SIMPLE_METHOD o record_auto_tac) *}
+method_setup record_auto = \<open>Scan.succeed (SIMPLE_METHOD o record_auto_tac)\<close>
 
 lemma inj_sysOfAlloc [iff]: "inj sysOfAlloc"
   apply (unfold sysOfAlloc_def Let_def)
@@ -346,7 +346,7 @@
   apply record_auto
   done
 
-text{*We need the inverse; also having it simplifies the proof of surjectivity*}
+text\<open>We need the inverse; also having it simplifies the proof of surjectivity\<close>
 lemma inv_sysOfAlloc_eq [simp]: "!!s. inv sysOfAlloc s =
              (| allocGiv = allocGiv s,
                 allocAsk = allocAsk s,
@@ -366,7 +366,7 @@
   done
 
 
-subsubsection{*bijectivity of @{term sysOfClient}*}
+subsubsection\<open>bijectivity of @{term sysOfClient}\<close>
 
 lemma inj_sysOfClient [iff]: "inj sysOfClient"
   apply (unfold sysOfClient_def)
@@ -394,7 +394,7 @@
   done
 
 
-subsubsection{*bijectivity of @{term client_map}*}
+subsubsection\<open>bijectivity of @{term client_map}\<close>
 
 lemma inj_client_map [iff]: "inj client_map"
   apply (unfold inj_on_def)
@@ -418,14 +418,14 @@
   done
 
 
-text{*o-simprules for @{term client_map}*}
+text\<open>o-simprules for @{term client_map}\<close>
 
 lemma fst_o_client_map: "fst o client_map = non_dummy"
   apply (unfold client_map_def)
   apply (rule fst_o_funPair)
   done
 
-ML {* ML_Thms.bind_thms ("fst_o_client_map'", make_o_equivs @{context} @{thm fst_o_client_map}) *}
+ML \<open>ML_Thms.bind_thms ("fst_o_client_map'", make_o_equivs @{context} @{thm fst_o_client_map})\<close>
 declare fst_o_client_map' [simp]
 
 lemma snd_o_client_map: "snd o client_map = clientState_d.dummy"
@@ -433,90 +433,90 @@
   apply (rule snd_o_funPair)
   done
 
-ML {* ML_Thms.bind_thms ("snd_o_client_map'", make_o_equivs @{context} @{thm snd_o_client_map}) *}
+ML \<open>ML_Thms.bind_thms ("snd_o_client_map'", make_o_equivs @{context} @{thm snd_o_client_map})\<close>
 declare snd_o_client_map' [simp]
 
 
-subsection{*o-simprules for @{term sysOfAlloc} [MUST BE AUTOMATED]*}
+subsection\<open>o-simprules for @{term sysOfAlloc} [MUST BE AUTOMATED]\<close>
 
 lemma client_o_sysOfAlloc: "client o sysOfAlloc = fst o allocState_d.dummy "
   apply record_auto
   done
 
-ML {* ML_Thms.bind_thms ("client_o_sysOfAlloc'", make_o_equivs @{context} @{thm client_o_sysOfAlloc}) *}
+ML \<open>ML_Thms.bind_thms ("client_o_sysOfAlloc'", make_o_equivs @{context} @{thm client_o_sysOfAlloc})\<close>
 declare client_o_sysOfAlloc' [simp]
 
 lemma allocGiv_o_sysOfAlloc_eq: "allocGiv o sysOfAlloc = allocGiv"
   apply record_auto
   done
 
-ML {* ML_Thms.bind_thms ("allocGiv_o_sysOfAlloc_eq'", make_o_equivs @{context} @{thm allocGiv_o_sysOfAlloc_eq}) *}
+ML \<open>ML_Thms.bind_thms ("allocGiv_o_sysOfAlloc_eq'", make_o_equivs @{context} @{thm allocGiv_o_sysOfAlloc_eq})\<close>
 declare allocGiv_o_sysOfAlloc_eq' [simp]
 
 lemma allocAsk_o_sysOfAlloc_eq: "allocAsk o sysOfAlloc = allocAsk"
   apply record_auto
   done
 
-ML {* ML_Thms.bind_thms ("allocAsk_o_sysOfAlloc_eq'", make_o_equivs @{context} @{thm allocAsk_o_sysOfAlloc_eq}) *}
+ML \<open>ML_Thms.bind_thms ("allocAsk_o_sysOfAlloc_eq'", make_o_equivs @{context} @{thm allocAsk_o_sysOfAlloc_eq})\<close>
 declare allocAsk_o_sysOfAlloc_eq' [simp]
 
 lemma allocRel_o_sysOfAlloc_eq: "allocRel o sysOfAlloc = allocRel"
   apply record_auto
   done
 
-ML {* ML_Thms.bind_thms ("allocRel_o_sysOfAlloc_eq'", make_o_equivs @{context} @{thm allocRel_o_sysOfAlloc_eq}) *}
+ML \<open>ML_Thms.bind_thms ("allocRel_o_sysOfAlloc_eq'", make_o_equivs @{context} @{thm allocRel_o_sysOfAlloc_eq})\<close>
 declare allocRel_o_sysOfAlloc_eq' [simp]
 
 
-subsection{* o-simprules for @{term sysOfClient} [MUST BE AUTOMATED]*}
+subsection\<open>o-simprules for @{term sysOfClient} [MUST BE AUTOMATED]\<close>
 
 lemma client_o_sysOfClient: "client o sysOfClient = fst"
   apply record_auto
   done
 
-ML {* ML_Thms.bind_thms ("client_o_sysOfClient'", make_o_equivs @{context} @{thm client_o_sysOfClient}) *}
+ML \<open>ML_Thms.bind_thms ("client_o_sysOfClient'", make_o_equivs @{context} @{thm client_o_sysOfClient})\<close>
 declare client_o_sysOfClient' [simp]
 
 lemma allocGiv_o_sysOfClient_eq: "allocGiv o sysOfClient = allocGiv o snd "
   apply record_auto
   done
 
-ML {* ML_Thms.bind_thms ("allocGiv_o_sysOfClient_eq'", make_o_equivs @{context} @{thm allocGiv_o_sysOfClient_eq}) *}
+ML \<open>ML_Thms.bind_thms ("allocGiv_o_sysOfClient_eq'", make_o_equivs @{context} @{thm allocGiv_o_sysOfClient_eq})\<close>
 declare allocGiv_o_sysOfClient_eq' [simp]
 
 lemma allocAsk_o_sysOfClient_eq: "allocAsk o sysOfClient = allocAsk o snd "
   apply record_auto
   done
 
-ML {* ML_Thms.bind_thms ("allocAsk_o_sysOfClient_eq'", make_o_equivs @{context} @{thm allocAsk_o_sysOfClient_eq}) *}
+ML \<open>ML_Thms.bind_thms ("allocAsk_o_sysOfClient_eq'", make_o_equivs @{context} @{thm allocAsk_o_sysOfClient_eq})\<close>
 declare allocAsk_o_sysOfClient_eq' [simp]
 
 lemma allocRel_o_sysOfClient_eq: "allocRel o sysOfClient = allocRel o snd "
   apply record_auto
   done
 
-ML {* ML_Thms.bind_thms ("allocRel_o_sysOfClient_eq'", make_o_equivs @{context} @{thm allocRel_o_sysOfClient_eq}) *}
+ML \<open>ML_Thms.bind_thms ("allocRel_o_sysOfClient_eq'", make_o_equivs @{context} @{thm allocRel_o_sysOfClient_eq})\<close>
 declare allocRel_o_sysOfClient_eq' [simp]
 
 lemma allocGiv_o_inv_sysOfAlloc_eq: "allocGiv o inv sysOfAlloc = allocGiv"
   apply (simp add: o_def)
   done
 
-ML {* ML_Thms.bind_thms ("allocGiv_o_inv_sysOfAlloc_eq'", make_o_equivs @{context} @{thm allocGiv_o_inv_sysOfAlloc_eq}) *}
+ML \<open>ML_Thms.bind_thms ("allocGiv_o_inv_sysOfAlloc_eq'", make_o_equivs @{context} @{thm allocGiv_o_inv_sysOfAlloc_eq})\<close>
 declare allocGiv_o_inv_sysOfAlloc_eq' [simp]
 
 lemma allocAsk_o_inv_sysOfAlloc_eq: "allocAsk o inv sysOfAlloc = allocAsk"
   apply (simp add: o_def)
   done
 
-ML {* ML_Thms.bind_thms ("allocAsk_o_inv_sysOfAlloc_eq'", make_o_equivs @{context} @{thm allocAsk_o_inv_sysOfAlloc_eq}) *}
+ML \<open>ML_Thms.bind_thms ("allocAsk_o_inv_sysOfAlloc_eq'", make_o_equivs @{context} @{thm allocAsk_o_inv_sysOfAlloc_eq})\<close>
 declare allocAsk_o_inv_sysOfAlloc_eq' [simp]
 
 lemma allocRel_o_inv_sysOfAlloc_eq: "allocRel o inv sysOfAlloc = allocRel"
   apply (simp add: o_def)
   done
 
-ML {* ML_Thms.bind_thms ("allocRel_o_inv_sysOfAlloc_eq'", make_o_equivs @{context} @{thm allocRel_o_inv_sysOfAlloc_eq}) *}
+ML \<open>ML_Thms.bind_thms ("allocRel_o_inv_sysOfAlloc_eq'", make_o_equivs @{context} @{thm allocRel_o_inv_sysOfAlloc_eq})\<close>
 declare allocRel_o_inv_sysOfAlloc_eq' [simp]
 
 lemma rel_inv_client_map_drop_map: "(rel o inv client_map o drop_map i o inv sysOfClient) =
@@ -524,7 +524,7 @@
   apply (simp add: o_def drop_map_def)
   done
 
-ML {* ML_Thms.bind_thms ("rel_inv_client_map_drop_map'", make_o_equivs @{context} @{thm rel_inv_client_map_drop_map}) *}
+ML \<open>ML_Thms.bind_thms ("rel_inv_client_map_drop_map'", make_o_equivs @{context} @{thm rel_inv_client_map_drop_map})\<close>
 declare rel_inv_client_map_drop_map [simp]
 
 lemma ask_inv_client_map_drop_map: "(ask o inv client_map o drop_map i o inv sysOfClient) =
@@ -532,17 +532,17 @@
   apply (simp add: o_def drop_map_def)
   done
 
-ML {* ML_Thms.bind_thms ("ask_inv_client_map_drop_map'", make_o_equivs @{context} @{thm ask_inv_client_map_drop_map}) *}
+ML \<open>ML_Thms.bind_thms ("ask_inv_client_map_drop_map'", make_o_equivs @{context} @{thm ask_inv_client_map_drop_map})\<close>
 declare ask_inv_client_map_drop_map [simp]
 
 
-text{*Client : <unfolded specification> *}
+text\<open>Client : <unfolded specification>\<close>
 lemmas client_spec_simps =
   client_spec_def client_increasing_def client_bounded_def
   client_progress_def client_allowed_acts_def client_preserves_def
   guarantees_Int_right
 
-ML {*
+ML \<open>
 val [Client_Increasing_ask, Client_Increasing_rel,
      Client_Bounded, Client_Progress, Client_AllowedActs,
      Client_preserves_giv, Client_preserves_dummy] =
@@ -556,7 +556,7 @@
 ML_Thms.bind_thm ("Client_AllowedActs", Client_AllowedActs);
 ML_Thms.bind_thm ("Client_preserves_giv", Client_preserves_giv);
 ML_Thms.bind_thm ("Client_preserves_dummy", Client_preserves_dummy);
-*}
+\<close>
 
 declare
   Client_Increasing_ask [iff]
@@ -566,13 +566,13 @@
   Client_preserves_dummy [iff]
 
 
-text{*Network : <unfolded specification> *}
+text\<open>Network : <unfolded specification>\<close>
 lemmas network_spec_simps =
   network_spec_def network_ask_def network_giv_def
   network_rel_def network_allowed_acts_def network_preserves_def
   ball_conj_distrib
 
-ML {*
+ML \<open>
 val [Network_Ask, Network_Giv, Network_Rel, Network_AllowedActs,
      Network_preserves_allocGiv, Network_preserves_rel,
      Network_preserves_ask]  =
@@ -586,7 +586,7 @@
 ML_Thms.bind_thm ("Network_preserves_allocGiv", Network_preserves_allocGiv);
 ML_Thms.bind_thm ("Network_preserves_rel", Network_preserves_rel);
 ML_Thms.bind_thm ("Network_preserves_ask", Network_preserves_ask);
-*}
+\<close>
 
 declare Network_preserves_allocGiv [iff]
 
@@ -598,12 +598,12 @@
   Network_preserves_rel [simplified o_def, simp]
   Network_preserves_ask [simplified o_def, simp]
 
-text{*Alloc : <unfolded specification> *}
+text\<open>Alloc : <unfolded specification>\<close>
 lemmas alloc_spec_simps =
   alloc_spec_def alloc_increasing_def alloc_safety_def
   alloc_progress_def alloc_allowed_acts_def alloc_preserves_def
 
-ML {*
+ML \<open>
 val [Alloc_Increasing_0, Alloc_Safety, Alloc_Progress, Alloc_AllowedActs,
      Alloc_preserves_allocRel, Alloc_preserves_allocAsk,
      Alloc_preserves_dummy] =
@@ -617,9 +617,9 @@
 ML_Thms.bind_thm ("Alloc_preserves_allocRel", Alloc_preserves_allocRel);
 ML_Thms.bind_thm ("Alloc_preserves_allocAsk", Alloc_preserves_allocAsk);
 ML_Thms.bind_thm ("Alloc_preserves_dummy", Alloc_preserves_dummy);
-*}
+\<close>
 
-text{*Strip off the INT in the guarantees postcondition*}
+text\<open>Strip off the INT in the guarantees postcondition\<close>
 
 lemmas Alloc_Increasing = Alloc_Increasing_0 [normalized]
 
@@ -629,7 +629,7 @@
   Alloc_preserves_dummy [iff]
 
 
-subsection{*Components Lemmas [MUST BE AUTOMATED]*}
+subsection\<open>Components Lemmas [MUST BE AUTOMATED]\<close>
 
 lemma Network_component_System: "Network \<squnion>
       ((rename sysOfClient
@@ -654,7 +654,7 @@
   Alloc_component_System [iff]
 
 
-text{** These preservation laws should be generated automatically **}
+text\<open>* These preservation laws should be generated automatically *\<close>
 
 lemma Client_Allowed [simp]: "Allowed Client = preserves rel Int preserves ask"
   by (auto simp add: Allowed_def Client_AllowedActs safety_prop_Acts_iff)
@@ -667,7 +667,7 @@
 lemma Alloc_Allowed [simp]: "Allowed Alloc = preserves allocGiv"
   by (auto simp add: Allowed_def Alloc_AllowedActs safety_prop_Acts_iff)
 
-text{*needed in @{text rename_client_map_tac}*}
+text\<open>needed in \<open>rename_client_map_tac\<close>\<close>
 lemma OK_lift_rename_Client [simp]: "OK I (%i. lift i (rename client_map Client))"
   apply (rule OK_lift_I)
   apply auto
@@ -708,7 +708,7 @@
 ad-hoc!
 *)
 ML
-{*
+\<open>
 fun rename_client_map_tac ctxt =
   EVERY [
     simp_tac (ctxt addsimps [@{thm rename_guarantees_eq_rename_inv}]) 1,
@@ -724,13 +724,13 @@
                       @{thm inv_inv_eq}]) 1,
     asm_simp_tac
         (ctxt addsimps [@{thm o_def}, @{thm non_dummy_def}, @{thm guarantees_Int_right}]) 1]
-*}
+\<close>
 
-method_setup rename_client_map = {*
+method_setup rename_client_map = \<open>
   Scan.succeed (fn ctxt => SIMPLE_METHOD (rename_client_map_tac ctxt))
-*}
+\<close>
 
-text{*Lifting @{text Client_Increasing} to @{term systemState}*}
+text\<open>Lifting \<open>Client_Increasing\<close> to @{term systemState}\<close>
 lemma rename_Client_Increasing: "i : I
       ==> rename sysOfClient (plam x: I. rename client_map Client) :
             UNIV  guarantees
@@ -772,8 +772,8 @@
   rename_sysOfClient_ok_Alloc [iff]
   rename_sysOfAlloc_ok_Network [iff]
 
-text{*The "ok" laws, re-oriented.
-  But not sure this works: theorem @{text ok_commute} is needed below*}
+text\<open>The "ok" laws, re-oriented.
+  But not sure this works: theorem \<open>ok_commute\<close> is needed below\<close>
 declare
   rename_sysOfClient_ok_Network [THEN ok_sym, iff]
   rename_sysOfClient_ok_Alloc [THEN ok_sym, iff]
@@ -807,15 +807,15 @@
   done
 
 
-ML {*
+ML \<open>
 ML_Thms.bind_thms ("System_Increasing'", list_of_Int @{thm System_Increasing})
-*}
+\<close>
 
 declare System_Increasing' [intro!]
 
-text{* Follows consequences.
+text\<open>Follows consequences.
     The "Always (INT ...) formulation expresses the general safety property
-    and allows it to be combined using @{text Always_Int_rule} below. *}
+    and allows it to be combined using \<open>Always_Int_rule\<close> below.\<close>
 
 lemma System_Follows_rel:
   "i < Nclients ==> System : ((sub i o allocRel) Fols (rel o sub i o client))"
@@ -857,11 +857,11 @@
   by (auto intro!: Follows_Bounded System_Follows_rel)
 
 
-subsection{*Proof of the safety property (1)*}
+subsection\<open>Proof of the safety property (1)\<close>
 
-text{*safety (1), step 1 is @{text System_Follows_rel}*}
+text\<open>safety (1), step 1 is \<open>System_Follows_rel\<close>\<close>
 
-text{*safety (1), step 2*}
+text\<open>safety (1), step 2\<close>
 (* i < Nclients ==> System : Increasing (sub i o allocRel) *)
 lemmas System_Increasing_allocRel = System_Follows_rel [THEN Follows_Increasing1]
 
@@ -869,7 +869,7 @@
   Simplifying with o_def gets rid of the translations but it unfortunately
   gets rid of the other "o"s too.*)
 
-text{*safety (1), step 3*}
+text\<open>safety (1), step 3\<close>
 lemma System_sum_bounded:
     "System : Always {s. (\<Sum>i \<in> lessThan Nclients. (tokens o sub i o allocGiv) s)
             \<le> NbT + (\<Sum>i \<in> lessThan Nclients. (tokens o sub i o allocRel) s)}"
@@ -880,7 +880,7 @@
   apply (auto simp add: System_Increasing_allocRel [simplified sub_apply o_def])
   done
 
-text{* Follows reasoning*}
+text\<open>Follows reasoning\<close>
 
 lemma Always_tokens_giv_le_allocGiv: "System : Always (INT i: lessThan Nclients.
                           {s. (tokens o giv o sub i o client) s
@@ -896,12 +896,12 @@
   apply (auto intro: tokens_mono_prefix simp add: o_apply)
   done
 
-text{*safety (1), step 4 (final result!) *}
+text\<open>safety (1), step 4 (final result!)\<close>
 theorem System_safety: "System : system_safety"
   apply (unfold system_safety_def)
-  apply (tactic {* resolve_tac @{context} [Always_Int_rule [@{thm System_sum_bounded},
+  apply (tactic \<open>resolve_tac @{context} [Always_Int_rule [@{thm System_sum_bounded},
     @{thm Always_tokens_giv_le_allocGiv}, @{thm Always_tokens_allocRel_le_rel}] RS
-    @{thm Always_weaken}] 1 *})
+    @{thm Always_weaken}] 1\<close>)
   apply auto
   apply (rule setsum_fun_mono [THEN order_trans])
   apply (drule_tac [2] order_trans)
@@ -910,16 +910,16 @@
   apply auto
   done
 
-subsection {* Proof of the progress property (2) *}
+subsection \<open>Proof of the progress property (2)\<close>
 
-text{*progress (2), step 1 is @{text System_Follows_ask} and
-      @{text System_Follows_rel}*}
+text\<open>progress (2), step 1 is \<open>System_Follows_ask\<close> and
+      \<open>System_Follows_rel\<close>\<close>
 
-text{*progress (2), step 2; see also @{text System_Increasing_allocRel}*}
+text\<open>progress (2), step 2; see also \<open>System_Increasing_allocRel\<close>\<close>
 (* i < Nclients ==> System : Increasing (sub i o allocAsk) *)
 lemmas System_Increasing_allocAsk =  System_Follows_ask [THEN Follows_Increasing1]
 
-text{*progress (2), step 3: lifting @{text Client_Bounded} to systemState*}
+text\<open>progress (2), step 3: lifting \<open>Client_Bounded\<close> to systemState\<close>
 lemma rename_Client_Bounded: "i : I
     ==> rename sysOfClient (plam x: I. rename client_map Client) :
           UNIV  guarantees
@@ -938,18 +938,18 @@
   apply blast
   done
 
-text{*progress (2), step 4*}
+text\<open>progress (2), step 4\<close>
 lemma System_Bounded_allocAsk: "System : Always {s. ALL i<Nclients.
                           ALL elt : set ((sub i o allocAsk) s). elt \<le> NbT}"
   apply (auto simp add: Collect_all_imp_eq)
-  apply (tactic {* resolve_tac @{context} [Always_Int_rule [@{thm Always_allocAsk_le_ask},
-    @{thm System_Bounded_ask}] RS @{thm Always_weaken}] 1 *})
+  apply (tactic \<open>resolve_tac @{context} [Always_Int_rule [@{thm Always_allocAsk_le_ask},
+    @{thm System_Bounded_ask}] RS @{thm Always_weaken}] 1\<close>)
   apply (auto dest: set_mono)
   done
 
-text{*progress (2), step 5 is @{text System_Increasing_allocGiv}*}
+text\<open>progress (2), step 5 is \<open>System_Increasing_allocGiv\<close>\<close>
 
-text{*progress (2), step 6*}
+text\<open>progress (2), step 6\<close>
 (* i < Nclients ==> System : Increasing (giv o sub i o client) *)
 lemmas System_Increasing_giv =  System_Follows_allocGiv [THEN Follows_Increasing1]
 
@@ -966,7 +966,7 @@
   done
 
 
-text{*progress (2), step 7*}
+text\<open>progress (2), step 7\<close>
 lemma System_Client_Progress:
   "System : (INT i : (lessThan Nclients).
             INT h. {s. h \<le> (giv o sub i o client) s &
@@ -1007,7 +1007,7 @@
   done
 
 
-text{*progress (2), step 8: Client i's "release" action is visible system-wide*}
+text\<open>progress (2), step 8: Client i's "release" action is visible system-wide\<close>
 lemma System_Alloc_Client_Progress: "i < Nclients
       ==> System : {s. h \<le> (sub i o allocGiv) s &
                        h pfixGe (sub i o allocAsk) s}
@@ -1025,9 +1025,9 @@
   apply (erule System_lemma3)
   done
 
-text{*Lifting @{text Alloc_Progress} up to the level of systemState*}
+text\<open>Lifting \<open>Alloc_Progress\<close> up to the level of systemState\<close>
 
-text{*progress (2), step 9*}
+text\<open>progress (2), step 9\<close>
 lemma System_Alloc_Progress:
  "System : (INT i : (lessThan Nclients).
             INT h. {s. h \<le> (sub i o allocAsk) s}
@@ -1043,7 +1043,7 @@
     System_Alloc_Client_Progress [simplified sub_apply o_def])
   done
 
-text{*progress (2), step 10 (final result!) *}
+text\<open>progress (2), step 10 (final result!)\<close>
 lemma System_Progress: "System : system_progress"
   apply (unfold system_progress_def)
   apply (cut_tac System_Alloc_Progress)
@@ -1060,7 +1060,7 @@
   done
 
 
-text{* Some obsolete lemmas *}
+text\<open>Some obsolete lemmas\<close>
 
 lemma non_dummy_eq_o_funPair: "non_dummy = (% (g,a,r). (| giv = g, ask = a, rel = r |)) o
                               (funPair giv (funPair ask rel))"
@@ -1078,7 +1078,7 @@
     apply (auto simp add: o_def)
   done
 
-text{*Could go to Extend.ML*}
+text\<open>Could go to Extend.ML\<close>
 lemma bij_fst_inv_inv_eq: "bij f ==> fst (inv (%(x, u). inv f x) z) = f z"
   apply (rule fst_inv_equalityI)
    apply (rule_tac f = "%z. (f z, h z)" for h in surjI)
diff -r 703edebd1d92 -r f1ecba0272f9 src/HOL/UNITY/Comp/AllocBase.thy
--- a/src/HOL/UNITY/Comp/AllocBase.thy	Wed May 25 11:49:40 2016 +0200
+++ b/src/HOL/UNITY/Comp/AllocBase.thy	Wed May 25 11:50:58 2016 +0200
@@ -3,7 +3,7 @@
     Copyright   1998  University of Cambridge
 *)
 
-section{*Common Declarations for Chandy and Charpentier's Allocator*}
+section\<open>Common Declarations for Chandy and Charpentier's Allocator\<close>
 
 theory AllocBase imports "../UNITY_Main" "~~/src/HOL/Library/Multiset_Order" begin
 
diff -r 703edebd1d92 -r f1ecba0272f9 src/HOL/UNITY/Comp/AllocImpl.thy
--- a/src/HOL/UNITY/Comp/AllocImpl.thy	Wed May 25 11:49:40 2016 +0200
+++ b/src/HOL/UNITY/Comp/AllocImpl.thy	Wed May 25 11:50:58 2016 +0200
@@ -3,7 +3,7 @@
     Copyright   1998  University of Cambridge
 *)
 
-section{*Implementation of a multiple-client allocator from a single-client allocator*}
+section\<open>Implementation of a multiple-client allocator from a single-client allocator\<close>
 
 theory AllocImpl imports AllocBase "../Follows" "../PPROD" begin
 
@@ -238,7 +238,7 @@
 declare o_apply [simp del]
 
 
-subsection{*Theorems for Merge*}
+subsection\<open>Theorems for Merge\<close>
 
 context Merge
 begin
@@ -307,7 +307,7 @@
 end
 
 
-subsection{*Theorems for Distributor*}
+subsection\<open>Theorems for Distributor\<close>
 
 context Distrib
 begin
@@ -371,7 +371,7 @@
 end
 
 
-subsection{*Theorems for Allocator*}
+subsection\<open>Theorems for Allocator\<close>
 
 lemma alloc_refinement_lemma:
      "!!f::nat=>nat. (\<Inter>i \<in> lessThan n. {s. f i \<le> g i s})
diff -r 703edebd1d92 -r f1ecba0272f9 src/HOL/UNITY/Comp/Client.thy
--- a/src/HOL/UNITY/Comp/Client.thy	Wed May 25 11:49:40 2016 +0200
+++ b/src/HOL/UNITY/Comp/Client.thy	Wed May 25 11:50:58 2016 +0200
@@ -3,22 +3,22 @@
     Copyright   1998  University of Cambridge
 *)
 
-section{*Distributed Resource Management System: the Client*}
+section\<open>Distributed Resource Management System: the Client\<close>
 
 theory Client imports "../Rename" AllocBase begin
 
 type_synonym
-  tokbag = nat     --{*tokbags could be multisets...or any ordered type?*}
+  tokbag = nat     \<comment>\<open>tokbags could be multisets...or any ordered type?\<close>
 
 record state =
-  giv :: "tokbag list" --{*input history: tokens granted*}
-  ask :: "tokbag list" --{*output history: tokens requested*}
-  rel :: "tokbag list" --{*output history: tokens released*}
-  tok :: tokbag        --{*current token request*}
+  giv :: "tokbag list" \<comment>\<open>input history: tokens granted\<close>
+  ask :: "tokbag list" \<comment>\<open>output history: tokens requested\<close>
+  rel :: "tokbag list" \<comment>\<open>output history: tokens released\<close>
+  tok :: tokbag        \<comment>\<open>current token request\<close>
 
 record 'a state_d =
   state +  
-  dummy :: 'a          --{*new variables*}
+  dummy :: 'a          \<comment>\<open>new variables\<close>
 
 
 (*Array indexing is translated to list indexing as A[n] == A!(n-1). *)
@@ -82,7 +82,7 @@
 by (auto simp add: ok_iff_Allowed Client_def [THEN def_total_prg_Allowed])
 
 
-text{*Safety property 1: ask, rel are increasing*}
+text\<open>Safety property 1: ask, rel are increasing\<close>
 lemma increasing_ask_rel:
      "Client \<in> UNIV guarantees Increasing ask Int Increasing rel"
 apply (auto intro!: increasing_imp_Increasing simp add: guar_def preserves_subset_increasing [THEN subsetD])
@@ -93,9 +93,9 @@
 declare nth_append [simp] append_one_prefix [simp]
 
 
-text{*Safety property 2: the client never requests too many tokens.
+text\<open>Safety property 2: the client never requests too many tokens.
       With no Substitution Axiom, we must prove the two invariants 
-      simultaneously. *}
+      simultaneously.\<close>
 lemma ask_bounded_lemma:
      "Client ok G   
       ==> Client \<squnion> G \<in>   
@@ -109,8 +109,8 @@
 apply (cut_tac m = "tok s" in NbT_pos [THEN mod_less_divisor], auto)
 done
 
-text{*export version, with no mention of tok in the postcondition, but
-  unfortunately tok must be declared local.*}
+text\<open>export version, with no mention of tok in the postcondition, but
+  unfortunately tok must be declared local.\<close>
 lemma ask_bounded:
      "Client \<in> UNIV guarantees Always {s. \<forall>elt \<in> set (ask s). elt \<le> NbT}"
 apply (rule guaranteesI)
@@ -119,7 +119,7 @@
 done
 
 
-text{*** Towards proving the liveness property ***}
+text\<open>** Towards proving the liveness property **\<close>
 
 lemma stable_rel_le_giv: "Client \<in> stable {s. rel s \<le> giv s}"
 by (simp add: Client_def, safety, auto)
@@ -189,7 +189,7 @@
 apply (blast intro: order_less_le [THEN iffD2] dest: common_prefix_linear)
 done
 
-text{*Progress property: all tokens that are given will be released*}
+text\<open>Progress property: all tokens that are given will be released\<close>
 lemma client_progress:
      "Client \<in>  
        Increasing giv  guarantees   
@@ -198,19 +198,19 @@
 apply (blast intro: client_progress_lemma)
 done
 
-text{*This shows that the Client won't alter other variables in any state
-  that it is combined with*}
+text\<open>This shows that the Client won't alter other variables in any state
+  that it is combined with\<close>
 lemma client_preserves_dummy: "Client \<in> preserves dummy"
 by (simp add: Client_def preserves_def, clarify, safety, auto)
 
 
-text{** Obsolete lemmas from first version of the Client **}
+text\<open>* Obsolete lemmas from first version of the Client *\<close>
 
 lemma stable_size_rel_le_giv:
      "Client \<in> stable {s. size (rel s) \<le> size (giv s)}"
 by (simp add: Client_def, safety, auto)
 
-text{*clients return the right number of tokens*}
+text\<open>clients return the right number of tokens\<close>
 lemma ok_guar_rel_prefix_giv:
      "Client \<in> Increasing giv  guarantees  Always {s. rel s \<le> giv s}"
 apply (rule guaranteesI)
diff -r 703edebd1d92 -r f1ecba0272f9 src/HOL/UNITY/Comp/Counter.thy
--- a/src/HOL/UNITY/Comp/Counter.thy	Wed May 25 11:49:40 2016 +0200
+++ b/src/HOL/UNITY/Comp/Counter.thy	Wed May 25 11:50:58 2016 +0200
@@ -8,7 +8,7 @@
    Springer LNCS 1586 (1999), pages 1215-1227.
 *)
 
-section{*A Family of Similar Counters: Original Version*}
+section\<open>A Family of Similar Counters: Original Version\<close>
 
 theory Counter imports "../UNITY_Main" begin
 
diff -r 703edebd1d92 -r f1ecba0272f9 src/HOL/UNITY/Comp/Counterc.thy
--- a/src/HOL/UNITY/Comp/Counterc.thy	Wed May 25 11:49:40 2016 +0200
+++ b/src/HOL/UNITY/Comp/Counterc.thy	Wed May 25 11:50:58 2016 +0200
@@ -11,7 +11,7 @@
    Spriner LNCS 1586 (1999), pages 1215-1227.
 *)
 
-section{*A Family of Similar Counters: Version with Compatibility*}
+section\<open>A Family of Similar Counters: Version with Compatibility\<close>
 
 theory Counterc imports "../UNITY_Main" begin
 
diff -r 703edebd1d92 -r f1ecba0272f9 src/HOL/UNITY/Comp/Priority.thy
--- a/src/HOL/UNITY/Comp/Priority.thy	Wed May 25 11:49:40 2016 +0200
+++ b/src/HOL/UNITY/Comp/Priority.thy	Wed May 25 11:50:58 2016 +0200
@@ -3,41 +3,41 @@
     Copyright   2001  University of Cambridge
 *)
 
-section{*The priority system*}
+section\<open>The priority system\<close>
 
 theory Priority imports PriorityAux begin
 
-text{*From Charpentier and Chandy,
+text\<open>From Charpentier and Chandy,
 Examples of Program Composition Illustrating the Use of Universal Properties
    In J. Rolim (editor), Parallel and Distributed Processing,
-   Spriner LNCS 1586 (1999), pages 1215-1227.*}
+   Spriner LNCS 1586 (1999), pages 1215-1227.\<close>
 
 type_synonym state = "(vertex*vertex)set"
 type_synonym command = "vertex=>(state*state)set"
   
 consts
   init :: "(vertex*vertex)set"  
-  --{* the initial state *}
+  \<comment>\<open>the initial state\<close>
 
-text{*Following the definitions given in section 4.4 *}
+text\<open>Following the definitions given in section 4.4\<close>
 
 definition highest :: "[vertex, (vertex*vertex)set]=>bool"
   where "highest i r \<longleftrightarrow> A i r = {}"
-    --{* i has highest priority in r *}
+    \<comment>\<open>i has highest priority in r\<close>
   
 definition lowest :: "[vertex, (vertex*vertex)set]=>bool"
   where "lowest i r \<longleftrightarrow> R i r = {}"
-    --{* i has lowest priority in r *}
+    \<comment>\<open>i has lowest priority in r\<close>
 
 definition act :: command
   where "act i = {(s, s'). s'=reverse i s & highest i s}"
 
 definition Component :: "vertex=>state program"
   where "Component i = mk_total_program({init}, {act i}, UNIV)"
-    --{* All components start with the same initial state *}
+    \<comment>\<open>All components start with the same initial state\<close>
 
 
-text{*Some Abbreviations *}
+text\<open>Some Abbreviations\<close>
 definition Highest :: "vertex=>state set"
   where "Highest i = {s. highest i s}"
 
@@ -49,11 +49,11 @@
 
 
 definition Maximal :: "state set"
-    --{* Every ``above'' set has a maximal vertex*}
+    \<comment>\<open>Every ``above'' set has a maximal vertex\<close>
   where "Maximal = (\<Inter>i. {s. ~highest i s-->(\<exists>j \<in> above i  s. highest j s)})"
 
 definition Maximal' :: "state set"
-    --{* Maximal vertex: equivalent definition*}
+    \<comment>\<open>Maximal vertex: equivalent definition\<close>
   where "Maximal' = (\<Inter>i. Highest i Un (\<Union>j. {s. j \<in> above i s} Int Highest j))"
 
   
@@ -77,18 +77,18 @@
 
 
 
-subsection{*Component correctness proofs*}
+subsection\<open>Component correctness proofs\<close>
 
-text{* neighbors is stable  *}
+text\<open>neighbors is stable\<close>
 lemma Component_neighbors_stable: "Component i \<in> stable {s. neighbors k s = n}"
 by (simp add: Component_def, safety, auto)
 
-text{* property 4 *}
+text\<open>property 4\<close>
 lemma Component_waits_priority: "Component i: {s. ((i,j):s) = b} Int (- Highest i) co {s. ((i,j):s)=b}"
 by (simp add: Component_def, safety)
 
-text{* property 5: charpentier and Chandy mistakenly express it as
- 'transient Highest i'. Consider the case where i has neighbors *}
+text\<open>property 5: charpentier and Chandy mistakenly express it as
+ 'transient Highest i'. Consider the case where i has neighbors\<close>
 lemma Component_yields_priority: 
  "Component i: {s. neighbors i s \<noteq> {}} Int Highest i  
                ensures - Highest i"
@@ -96,23 +96,23 @@
 apply (ensures_tac "act i", blast+) 
 done
 
-text{* or better *}
+text\<open>or better\<close>
 lemma Component_yields_priority': "Component i \<in> Highest i ensures Lowest i"
 apply (simp add: Component_def)
 apply (ensures_tac "act i", blast+) 
 done
 
-text{* property 6: Component doesn't introduce cycle *}
+text\<open>property 6: Component doesn't introduce cycle\<close>
 lemma Component_well_behaves: "Component i \<in> Highest i co Highest i Un Lowest i"
 by (simp add: Component_def, safety, fast)
 
-text{* property 7: local axiom *}
+text\<open>property 7: local axiom\<close>
 lemma locality: "Component i \<in> stable {s. \<forall>j k. j\<noteq>i & k\<noteq>i--> ((j,k):s) = b j k}"
 by (simp add: Component_def, safety)
 
 
-subsection{*System  properties*}
-text{* property 8: strictly universal *}
+subsection\<open>System  properties\<close>
+text\<open>property 8: strictly universal\<close>
 
 lemma Safety: "system \<in> stable Safety"
 apply (unfold Safety_def)
@@ -120,12 +120,12 @@
 apply (simp add: system_def, safety, fast)
 done
 
-text{* property 13: universal *}
+text\<open>property 13: universal\<close>
 lemma p13: "system \<in> {s. s = q} co {s. s=q} Un {s. \<exists>i. derive i q s}"
 by (simp add: system_def Component_def mk_total_program_def totalize_JN, safety, blast)
 
-text{* property 14: the 'above set' of a Component that hasn't got 
-      priority doesn't increase *}
+text\<open>property 14: the 'above set' of a Component that hasn't got 
+      priority doesn't increase\<close>
 lemma above_not_increase: 
      "system \<in> -Highest i Int {s. j\<notin>above i s} co {s. j\<notin>above i s}"
 apply (insert reach_lemma [of concl: j])
@@ -142,7 +142,7 @@
 
 
 
-text{* p15: universal property: all Components well behave  *}
+text\<open>p15: universal property: all Components well behave\<close>
 lemma system_well_behaves: "system \<in> Highest i co Highest i Un Lowest i"
   by (simp add: system_def Component_def mk_total_program_def totalize_JN, safety, auto)
 
@@ -166,23 +166,23 @@
 apply (drule above_lemma_b, auto)
 done
 
-text{* property 17: original one is an invariant *}
+text\<open>property 17: original one is an invariant\<close>
 lemma Acyclic_Maximal_stable: "system \<in> stable (Acyclic Int Maximal)"
 by (simp add: Acyclic_subset_Maximal [THEN Int_absorb2] Acyclic_stable)
 
 
-text{* property 5: existential property *}
+text\<open>property 5: existential property\<close>
 
 lemma Highest_leadsTo_Lowest: "system \<in> Highest i leadsTo Lowest i"
 apply (simp add: system_def Component_def mk_total_program_def totalize_JN)
 apply (ensures_tac "act i", auto)
 done
 
-text{* a lowest i can never be in any abover set *} 
+text\<open>a lowest i can never be in any abover set\<close> 
 lemma Lowest_above_subset: "Lowest i <= (\<Inter>k. {s. i\<notin>above k s})"
 by (auto simp add: image0_r_iff_image0_trancl trancl_converse)
 
-text{* property 18: a simpler proof than the original, one which uses psp *}
+text\<open>property 18: a simpler proof than the original, one which uses psp\<close>
 lemma Highest_escapes_above: "system \<in> Highest i leadsTo (\<Inter>k. {s. i\<notin>above k s})"
 apply (rule leadsTo_weaken_R)
 apply (rule_tac [2] Lowest_above_subset)
@@ -193,9 +193,9 @@
      "system \<in> Highest j Int {s. j \<in> above i s} leadsTo {s. j\<notin>above i s}"
 by (blast intro: leadsTo_weaken [OF Highest_escapes_above Int_lower1 INT_lower])
 
-subsection{*The main result: above set decreases*}
+subsection\<open>The main result: above set decreases\<close>
 
-text{* The original proof of the following formula was wrong *}
+text\<open>The original proof of the following formula was wrong\<close>
 
 lemma Highest_iff_above0: "Highest i = {s. above i s ={}}"
 by (auto simp add: image0_trancl_iff_image0_r)
@@ -253,10 +253,10 @@
 done
 
 
-text{*We have proved all (relevant) theorems given in the paper.  We didn't
+text\<open>We have proved all (relevant) theorems given in the paper.  We didn't
 assume any thing about the relation @{term r}.  It is not necessary that
 @{term r} be a priority relation as assumed in the original proof.  It
-suffices that we start from a state which is finite and acyclic.*}
+suffices that we start from a state which is finite and acyclic.\<close>
 
 
 end
diff -r 703edebd1d92 -r f1ecba0272f9 src/HOL/UNITY/Comp/PriorityAux.thy
--- a/src/HOL/UNITY/Comp/PriorityAux.thy	Wed May 25 11:49:40 2016 +0200
+++ b/src/HOL/UNITY/Comp/PriorityAux.thy	Wed May 25 11:50:58 2016 +0200
@@ -13,11 +13,11 @@
   
 definition symcl :: "(vertex*vertex)set=>(vertex*vertex)set" where
   "symcl r == r \<union> (r^-1)"
-    --{* symmetric closure: removes the orientation of a relation*}
+    \<comment>\<open>symmetric closure: removes the orientation of a relation\<close>
 
 definition neighbors :: "[vertex, (vertex*vertex)set]=>vertex set" where
   "neighbors i r == ((r \<union> r^-1)``{i}) - {i}"
-    --{* Neighbors of a vertex i *}
+    \<comment>\<open>Neighbors of a vertex i\<close>
 
 definition R :: "[vertex, (vertex*vertex)set]=>vertex set" where
   "R i r == r``{i}"
@@ -27,7 +27,7 @@
 
 definition reach :: "[vertex, (vertex*vertex)set]=> vertex set" where
   "reach i r == (r^+)``{i}"
-    --{* reachable and above vertices: the original notation was R* and A* *}
+    \<comment>\<open>reachable and above vertices: the original notation was R* and A*\<close>
 
 definition above :: "[vertex, (vertex*vertex)set]=> vertex set" where
   "above i r == ((r^-1)^+)``{i}"  
@@ -36,28 +36,28 @@
   "reverse i r == (r - {(x,y). x=i | y=i} \<inter> r) \<union> ({(x,y). x=i|y=i} \<inter> r)^-1"
 
 definition derive1 :: "[vertex, (vertex*vertex)set, (vertex*vertex)set]=>bool" where
-    --{* The original definition *}
+    \<comment>\<open>The original definition\<close>
   "derive1 i r q == symcl r = symcl q &
                     (\<forall>k k'. k\<noteq>i & k'\<noteq>i -->((k,k'):r) = ((k,k'):q)) &
                     A i r = {} & R i q = {}"
 
 definition derive :: "[vertex, (vertex*vertex)set, (vertex*vertex)set]=>bool" where
-    --{* Our alternative definition *}
+    \<comment>\<open>Our alternative definition\<close>
   "derive i r q == A i r = {} & (q = reverse i r)"
 
 axiomatization where
   finite_vertex_univ:  "finite (UNIV :: vertex set)"
-    --{* we assume that the universe of vertices is finite  *}
+    \<comment>\<open>we assume that the universe of vertices is finite\<close>
 
 declare derive_def [simp] derive1_def [simp] symcl_def [simp] 
         A_def [simp] R_def [simp] 
         above_def [simp] reach_def [simp] 
         reverse_def [simp] neighbors_def [simp]
 
-text{*All vertex sets are finite*}
+text\<open>All vertex sets are finite\<close>
 declare finite_subset [OF subset_UNIV finite_vertex_univ, iff]
 
-text{* and relatons over vertex are finite too *}
+text\<open>and relatons over vertex are finite too\<close>
 
 lemmas finite_UNIV_Prod =
        finite_Prod_UNIV [OF finite_vertex_univ finite_vertex_univ] 
diff -r 703edebd1d92 -r f1ecba0272f9 src/HOL/UNITY/Comp/Progress.thy
--- a/src/HOL/UNITY/Comp/Progress.thy	Wed May 25 11:49:40 2016 +0200
+++ b/src/HOL/UNITY/Comp/Progress.thy	Wed May 25 11:50:58 2016 +0200
@@ -5,12 +5,12 @@
 David Meier's thesis
 *)
 
-section{*Progress Set Examples*}
+section\<open>Progress Set Examples\<close>
 
 theory Progress imports "../UNITY_Main" begin
 
-subsection {*The Composition of Two Single-Assignment Programs*}
-text{*Thesis Section 4.4.2*}
+subsection \<open>The Composition of Two Single-Assignment Programs\<close>
+text\<open>Thesis Section 4.4.2\<close>
 
 definition FF :: "int program" where
     "FF = mk_total_program (UNIV, {range (\<lambda>x. (x, x+1))}, UNIV)"
@@ -18,7 +18,7 @@
 definition GG :: "int program" where
     "GG = mk_total_program (UNIV, {range (\<lambda>x. (x, 2*x))}, UNIV)"
 
-subsubsection {*Calculating @{term "wens_set FF (atLeast k)"}*}
+subsubsection \<open>Calculating @{term "wens_set FF (atLeast k)"}\<close>
 
 lemma Domain_actFF: "Domain (range (\<lambda>x::int. (x, x + 1))) = UNIV"
 by force
@@ -62,7 +62,7 @@
 apply (simp add: wens_single_finite_FF)
 done
 
-subsubsection {*Proving @{term "FF \<in> UNIV leadsTo atLeast (k::int)"}*}
+subsubsection \<open>Proving @{term "FF \<in> UNIV leadsTo atLeast (k::int)"}\<close>
 
 lemma atLeast_ensures: "FF \<in> atLeast (k - 1) ensures atLeast (k::int)"
 apply (simp add: Progress.wens_FF [symmetric] wens_ensures)
@@ -86,7 +86,7 @@
 apply (rule leadsTo_UN [OF atLeast_leadsTo]) 
 done
 
-text{*Result (4.39): Applying the leadsTo-Join Theorem*}
+text\<open>Result (4.39): Applying the leadsTo-Join Theorem\<close>
 theorem "FF\<squnion>GG \<in> atLeast 0 leadsTo atLeast (k::int)"
 apply (subgoal_tac "FF\<squnion>GG \<in> (atLeast 0 \<inter> atLeast 0) leadsTo atLeast k")
  apply simp
diff -r 703edebd1d92 -r f1ecba0272f9 src/HOL/UNITY/Constrains.thy
--- a/src/HOL/UNITY/Constrains.thy	Wed May 25 11:49:40 2016 +0200
+++ b/src/HOL/UNITY/Constrains.thy	Wed May 25 11:50:58 2016 +0200
@@ -5,7 +5,7 @@
 Weak safety relations: restricted to the set of reachable states.
 *)
 
-section{*Weak Safety*}
+section\<open>Weak Safety\<close>
 
 theory Constrains imports UNITY begin
 
@@ -50,7 +50,7 @@
     "Increasing f == \<Inter>z. Stable {s. z \<le> f s}"
 
 
-subsection{*traces and reachable*}
+subsection\<open>traces and reachable\<close>
 
 lemma reachable_equiv_traces:
      "reachable F = {s. \<exists>evs. (s,evs) \<in> traces (Init F) (Acts F)}"
@@ -82,7 +82,7 @@
 done
 
 
-subsection{*Co*}
+subsection\<open>Co\<close>
 
 (*F \<in> B co B' ==> F \<in> (reachable F \<inter> B) co (reachable F \<inter> B')*)
 lemmas constrains_reachable_Int =  
@@ -185,7 +185,7 @@
 done
 
 
-subsection{*Stable*}
+subsection\<open>Stable\<close>
 
 (*Useful because there's no Stable_weaken.  [Tanja Vos]*)
 lemma Stable_eq: "[| F \<in> Stable A; A = B |] ==> F \<in> Stable B"
@@ -239,7 +239,7 @@
 
 
 
-subsection{*Increasing*}
+subsection\<open>Increasing\<close>
 
 lemma IncreasingD: 
      "F \<in> Increasing f ==> F \<in> Stable {s. x \<le> f s}"
@@ -265,7 +265,7 @@
 lemmas Increasing_constant = increasing_constant [THEN increasing_imp_Increasing, iff]
 
 
-subsection{*The Elimination Theorem*}
+subsection\<open>The Elimination Theorem\<close>
 
 (*The "free" m has become universally quantified! Should the premise be !!m
 instead of \<forall>m ?  Would make it harder to use in forward proof.*)
@@ -282,7 +282,7 @@
 by (unfold Constrains_def constrains_def, blast)
 
 
-subsection{*Specialized laws for handling Always*}
+subsection\<open>Specialized laws for handling Always\<close>
 
 (** Natural deduction rules for "Always A" **)
 
@@ -339,7 +339,7 @@
 by (auto simp add: Always_eq_includes_reachable)
 
 
-subsection{*"Co" rules involving Always*}
+subsection\<open>"Co" rules involving Always\<close>
 
 lemma Always_Constrains_pre:
      "F \<in> Always INV ==> (F \<in> (INV \<inter> A) Co A') = (F \<in> A Co A')"
@@ -390,7 +390,7 @@
 lemmas Always_thin = thin_rl [of "F \<in> Always A"]
 
 
-subsection{*Totalize*}
+subsection\<open>Totalize\<close>
 
 lemma reachable_imp_reachable_tot:
       "s \<in> reachable F ==> s \<in> reachable (totalize F)"
diff -r 703edebd1d92 -r f1ecba0272f9 src/HOL/UNITY/Detects.thy
--- a/src/HOL/UNITY/Detects.thy	Wed May 25 11:49:40 2016 +0200
+++ b/src/HOL/UNITY/Detects.thy	Wed May 25 11:50:58 2016 +0200
@@ -5,7 +5,7 @@
 Detects definition (Section 3.8 of Chandy & Misra) using LeadsTo
 *)
 
-section{*The Detects Relation*}
+section\<open>The Detects Relation\<close>
 
 theory Detects imports FP SubstAx begin
 
diff -r 703edebd1d92 -r f1ecba0272f9 src/HOL/UNITY/ELT.thy
--- a/src/HOL/UNITY/ELT.thy	Wed May 25 11:49:40 2016 +0200
+++ b/src/HOL/UNITY/ELT.thy	Wed May 25 11:50:58 2016 +0200
@@ -21,7 +21,7 @@
   monos Pow_mono
 *)
 
-section{*Progress Under Allowable Sets*}
+section\<open>Progress Under Allowable Sets\<close>
 
 theory ELT imports Project begin
 
diff -r 703edebd1d92 -r f1ecba0272f9 src/HOL/UNITY/Extend.thy
--- a/src/HOL/UNITY/Extend.thy	Wed May 25 11:49:40 2016 +0200
+++ b/src/HOL/UNITY/Extend.thy	Wed May 25 11:50:58 2016 +0200
@@ -7,7 +7,7 @@
   function g (forgotten) maps the extended state to the "extending part"
 *)
 
-section{*Extending State Sets*}
+section\<open>Extending State Sets\<close>
 
 theory Extend imports Guar begin
 
@@ -67,7 +67,7 @@
 (** These we prove OUTSIDE the locale. **)
 
 
-subsection{*Restrict*}
+subsection\<open>Restrict\<close>
 (*MOVE to Relation.thy?*)
 
 lemma Restrict_iff [iff]: "((x,y): Restrict A r) = ((x,y): r & x \<in> A)"
@@ -130,7 +130,7 @@
 by (metis UNIV_I f_inv_into_f prod.collapse prem surj_h)
 
 
-subsection{*Trivial properties of f, g, h*}
+subsection\<open>Trivial properties of f, g, h\<close>
 
 context Extend
 begin
@@ -167,7 +167,7 @@
 end
 
 
-subsection{*@{term extend_set}: basic properties*}
+subsection\<open>@{term extend_set}: basic properties\<close>
 
 lemma project_set_iff [iff]:
      "(x \<in> project_set h C) = (\<exists>y. h(x,y) \<in> C)"
@@ -215,7 +215,7 @@
 apply (auto simp add: split_extended_all)
 done
 
-subsection{*@{term project_set}: basic properties*}
+subsection\<open>@{term project_set}: basic properties\<close>
 
 (*project_set is simply image!*)
 lemma project_set_eq: "project_set h C = f ` C"
@@ -226,7 +226,7 @@
 by (auto simp add: split_extended_all)
 
 
-subsection{*More laws*}
+subsection\<open>More laws\<close>
 
 (*Because A and B could differ on the "other" part of the state, 
    cannot generalize to 
@@ -262,7 +262,7 @@
   by (auto simp: extend_set_def)
 
 
-subsection{*@{term extend_act}*}
+subsection\<open>@{term extend_act}\<close>
 
 (*Can't strengthen it to
   ((h(s,y), h(s',y')) \<in> extend_act h act) = ((s, s') \<in> act & y=y')
@@ -318,9 +318,9 @@
   unfolding project_act_def by (force simp add: split_extended_all)
 
 
-subsection{*extend*}
+subsection\<open>extend\<close>
 
-text{*Basic properties*}
+text\<open>Basic properties\<close>
 
 lemma (in -) Init_extend [simp]:
      "Init (extend h F) = extend_set h (Init F)"
@@ -431,7 +431,7 @@
 lemma all_total_extend: "all_total F ==> all_total (extend h F)"
   by (simp add: all_total_def Domain_extend_act)
 
-subsection{*Safety: co, stable*}
+subsection\<open>Safety: co, stable\<close>
 
 lemma extend_constrains:
      "(extend h F \<in> (extend_set h A) co (extend_set h B)) =  
@@ -457,7 +457,7 @@
   by (simp add: stable_def extend_constrains_project_set)
 
 
-subsection{*Weak safety primitives: Co, Stable*}
+subsection\<open>Weak safety primitives: Co, Stable\<close>
 
 lemma reachable_extend_f: "p \<in> reachable (extend h F) ==> f p \<in> reachable F"
   by (induct set: reachable) (auto intro: reachable.intros simp add: extend_act_def image_iff)
@@ -539,7 +539,7 @@
   by (simp add: stable_def project_constrains_project_set)
 
 
-subsection{*Progress: transient, ensures*}
+subsection\<open>Progress: transient, ensures\<close>
 
 lemma extend_transient:
      "(extend h F \<in> transient (extend_set h A)) = (F \<in> transient A)"
@@ -560,7 +560,7 @@
 apply (simp add: leadsTo_UN extend_set_Union)
 done
 
-subsection{*Proving the converse takes some doing!*}
+subsection\<open>Proving the converse takes some doing!\<close>
 
 lemma slice_iff [iff]: "(x \<in> slice C y) = (h(x,y) \<in> C)"
   by (simp add: slice_def)
@@ -621,7 +621,7 @@
               extend_set_Int_distrib [symmetric])
 
 
-subsection{*preserves*}
+subsection\<open>preserves\<close>
 
 lemma project_preserves_I:
      "G \<in> preserves (v o f) ==> project h C G \<in> preserves v"
@@ -642,7 +642,7 @@
                    constrains_def g_def)
 
 
-subsection{*Guarantees*}
+subsection\<open>Guarantees\<close>
 
 lemma project_extend_Join: "project h UNIV ((extend h F)\<squnion>G) = F\<squnion>(project h UNIV G)"
   apply (rule program_equalityI)
diff -r 703edebd1d92 -r f1ecba0272f9 src/HOL/UNITY/FP.thy
--- a/src/HOL/UNITY/FP.thy	Wed May 25 11:49:40 2016 +0200
+++ b/src/HOL/UNITY/FP.thy	Wed May 25 11:50:58 2016 +0200
@@ -5,7 +5,7 @@
 From Misra, "A Logic for Concurrent Programming", 1994
 *)
 
-section{*Fixed Point of a Program*}
+section\<open>Fixed Point of a Program\<close>
 
 theory FP imports UNITY begin
 
diff -r 703edebd1d92 -r f1ecba0272f9 src/HOL/UNITY/Follows.thy
--- a/src/HOL/UNITY/Follows.thy	Wed May 25 11:49:40 2016 +0200
+++ b/src/HOL/UNITY/Follows.thy	Wed May 25 11:50:58 2016 +0200
@@ -3,7 +3,7 @@
     Copyright   1998  University of Cambridge
 *)
 
-section{*The Follows Relation of Charpentier and Sivilotte*}
+section\<open>The Follows Relation of Charpentier and Sivilotte\<close>
 
 theory Follows
 imports SubstAx ListOrder "~~/src/HOL/Library/Multiset"
@@ -62,7 +62,7 @@
 done
 
 
-subsection{*Destruction rules*}
+subsection\<open>Destruction rules\<close>
 
 lemma Follows_Increasing1: "F \<in> f Fols g ==> F \<in> Increasing f"
 by (simp add: Follows_def)
@@ -118,7 +118,7 @@
 done
 
 
-subsection{*Union properties (with the subset ordering)*}
+subsection\<open>Union properties (with the subset ordering)\<close>
 
 (*Can replace "Un" by any sup.  But existing max only works for linorders.*)
 
@@ -174,7 +174,7 @@
 done
 
 
-subsection{*Multiset union properties (with the multiset ordering)*}
+subsection\<open>Multiset union properties (with the multiset ordering)\<close>
 (*TODO: remove when multiset is of sort ord again*)
 instantiation multiset :: (order) ordered_ab_semigroup_add
 begin
diff -r 703edebd1d92 -r f1ecba0272f9 src/HOL/UNITY/Guar.thy
--- a/src/HOL/UNITY/Guar.thy	Wed May 25 11:49:40 2016 +0200
+++ b/src/HOL/UNITY/Guar.thy	Wed May 25 11:50:58 2016 +0200
@@ -10,7 +10,7 @@
 Fifth International Conference on Mathematics of Program, 2000.
 *)
 
-section{*Guarantees Specifications*}
+section\<open>Guarantees Specifications\<close>
 
 theory Guar
 imports Comp
@@ -19,8 +19,8 @@
 instance program :: (type) order
   by standard (auto simp add: program_less_le dest: component_antisym intro: component_trans)
 
-text{*Existential and Universal properties.  I formalize the two-program
-      case, proving equivalence with Chandy and Sanders's n-ary definitions*}
+text\<open>Existential and Universal properties.  I formalize the two-program
+      case, proving equivalence with Chandy and Sanders's n-ary definitions\<close>
 
 definition ex_prop :: "'a program set => bool" where
    "ex_prop X == \<forall>F G. F ok G -->F \<in> X | G \<in> X --> (F\<squnion>G) \<in> X"
@@ -36,7 +36,7 @@
       SKIP \<in> X & (\<forall>F G. F ok G --> (F \<in> X & G \<in> X) = (F\<squnion>G \<in> X))"
 
 
-text{*Guarantees properties*}
+text\<open>Guarantees properties\<close>
 
 definition guar :: "['a program set, 'a program set] => 'a program set" (infixl "guarantees" 55) where
           (*higher than membership, lower than Co*)
@@ -73,7 +73,7 @@
 by (auto intro: ok_sym simp add: OK_iff_ok)
 
 
-subsection{*Existential Properties*}
+subsection\<open>Existential Properties\<close>
 
 lemma ex1:
   assumes "ex_prop X" and "finite GG"
@@ -110,7 +110,7 @@
 done
 
 
-subsection{*Universal Properties*}
+subsection\<open>Universal Properties\<close>
 
 lemma uv1:
   assumes "uv_prop X"
@@ -143,7 +143,7 @@
       (\<forall>GG. finite GG & GG \<subseteq> X & OK GG (%G. G) --> (\<Squnion>G \<in> GG. G): X)"
 by (blast intro: uv1 uv2)
 
-subsection{*Guarantees*}
+subsection\<open>Guarantees\<close>
 
 lemma guaranteesI:
      "(!!G. [| F ok G; F\<squnion>G \<in> X |] ==> F\<squnion>G \<in> Y) ==> F \<in> X guarantees Y"
@@ -191,7 +191,7 @@
 done
 
 
-subsection{*Distributive Laws.  Re-Orient to Perform Miniscoping*}
+subsection\<open>Distributive Laws.  Re-Orient to Perform Miniscoping\<close>
 
 lemma guarantees_UN_left: 
      "(\<Union>i \<in> I. X i) guarantees Y = (\<Inter>i \<in> I. X i guarantees Y)"
@@ -252,7 +252,7 @@
 by (unfold guar_def, blast)
 
 
-subsection{*Guarantees: Additional Laws (by lcp)*}
+subsection\<open>Guarantees: Additional Laws (by lcp)\<close>
 
 lemma guarantees_Join_Int: 
     "[| F \<in> U guarantees V;  G \<in> X guarantees Y; F ok G |]  
@@ -297,7 +297,7 @@
 done
 
 
-subsection{*Guarantees Laws for Breaking Down the Program (by lcp)*}
+subsection\<open>Guarantees Laws for Breaking Down the Program (by lcp)\<close>
 
 lemma guarantees_Join_I1: 
      "[| F \<in> X guarantees Y;  F ok G |] ==> F\<squnion>G \<in> X guarantees Y"
@@ -440,7 +440,7 @@
 apply (simp add: ok_commute  Join_ac) 
 done
 
-text{* Equivalence with the other definition of wx *}
+text\<open>Equivalence with the other definition of wx\<close>
 
 lemma wx_equiv: "wx X = {F. \<forall>G. F ok G --> (F\<squnion>G) \<in> X}"
 apply (unfold wx_def, safe)
@@ -453,9 +453,9 @@
 done
 
 
-text{* Propositions 7 to 11 are about this second definition of wx. 
+text\<open>Propositions 7 to 11 are about this second definition of wx. 
    They are the same as the ones proved for the first definition of wx,
- by equivalence *}
+ by equivalence\<close>
    
 (* Proposition 12 *)
 (* Main result of the paper *)
diff -r 703edebd1d92 -r f1ecba0272f9 src/HOL/UNITY/Lift_prog.thy
--- a/src/HOL/UNITY/Lift_prog.thy	Wed May 25 11:49:40 2016 +0200
+++ b/src/HOL/UNITY/Lift_prog.thy	Wed May 25 11:50:58 2016 +0200
@@ -5,7 +5,7 @@
 lift_prog, etc: replication of components and arrays of processes. 
 *)
 
-section{*Replication of Components*}
+section\<open>Replication of Components\<close>
 
 theory Lift_prog imports Rename begin
 
@@ -44,7 +44,7 @@
 apply (auto split add: nat_diff_split)
 done
 
-subsection{*Injectiveness proof*}
+subsection\<open>Injectiveness proof\<close>
 
 lemma insert_map_inject1: "(insert_map i x f) = (insert_map i y g) ==> x=y"
 by (drule_tac x = i in fun_cong, simp)
@@ -77,7 +77,7 @@
 apply (rule inj_onI, auto)
 done
 
-subsection{*Surjectiveness proof*}
+subsection\<open>Surjectiveness proof\<close>
 
 lemma lift_map_drop_map_eq [simp]: "!!s. lift_map i (drop_map i s) = s"
 apply (unfold lift_map_def drop_map_def)
@@ -121,7 +121,7 @@
        else insert_map j t (f(i - Suc 0 := s)))"
 apply (rule ext) 
 apply (simp split add: nat_diff_split)
- txt{*This simplification is VERY slow*}
+ txt\<open>This simplification is VERY slow\<close>
 done
 
 lemma insert_map_eq_diff:
@@ -140,7 +140,7 @@
 done
 
 
-subsection{*The Operator @{term lift_set}*}
+subsection\<open>The Operator @{term lift_set}\<close>
 
 lemma lift_set_empty [simp]: "lift_set i {} = {}"
 by (unfold lift_set_def, auto)
@@ -170,7 +170,7 @@
 done
 
 
-subsection{*The Lattice Operations*}
+subsection\<open>The Lattice Operations\<close>
 
 lemma bij_lift [iff]: "bij (lift i)"
 by (simp add: lift_def)
@@ -184,7 +184,7 @@
 lemma lift_JN [simp]: "lift j (JOIN I F) = (\<Squnion>i \<in> I. lift j (F i))"
 by (simp add: lift_def)
 
-subsection{*Safety: constrains, stable, invariant*}
+subsection\<open>Safety: constrains, stable, invariant\<close>
 
 lemma lift_constrains: 
      "(lift i F \<in> (lift_set i A) co (lift_set i B)) = (F \<in> A co B)"
@@ -210,7 +210,7 @@
      "(lift i F \<in> Always (lift_set i A)) = (F \<in> Always A)"
 by (simp add: lift_def lift_set_def rename_Always)
 
-subsection{*Progress: transient, ensures*}
+subsection\<open>Progress: transient, ensures\<close>
 
 lemma lift_transient: 
      "(lift i F \<in> transient (lift_set i A)) = (F \<in> transient A)"
@@ -333,7 +333,7 @@
 done
 
 
-subsection{*Lemmas to Handle Function Composition (o) More Consistently*}
+subsection\<open>Lemmas to Handle Function Composition (o) More Consistently\<close>
 
 (*Lets us prove one version of a theorem and store others*)
 lemma o_equiv_assoc: "f o g = h ==> f' o f o g = f' o h"
@@ -353,9 +353,9 @@
 done
 
 
-subsection{*More lemmas about extend and project*}
+subsection\<open>More lemmas about extend and project\<close>
 
-text{*They could be moved to theory Extend or Project*}
+text\<open>They could be moved to theory Extend or Project\<close>
 
 lemma extend_act_extend_act:
      "extend_act h' (extend_act h act) =  
@@ -375,7 +375,7 @@
 by (simp add: extend_act_def project_act_def, blast)
 
 
-subsection{*OK and "lift"*}
+subsection\<open>OK and "lift"\<close>
 
 lemma act_in_UNION_preserves_fst:
      "act \<subseteq> {(x,x'). fst x = fst x'} ==> act \<in> UNION (preserves fst) Acts"
diff -r 703edebd1d92 -r f1ecba0272f9 src/HOL/UNITY/ListOrder.thy
--- a/src/HOL/UNITY/ListOrder.thy	Wed May 25 11:49:40 2016 +0200
+++ b/src/HOL/UNITY/ListOrder.thy	Wed May 25 11:50:58 2016 +0200
@@ -10,7 +10,7 @@
 Also overloads <= and < for lists!
 *)
 
-section {*The Prefix Ordering on Lists*}
+section \<open>The Prefix Ordering on Lists\<close>
 
 theory ListOrder
 imports Main
@@ -57,7 +57,7 @@
   "xs pfixGe ys == (xs,ys) : genPrefix Ge"
 
 
-subsection{*preliminary lemmas*}
+subsection\<open>preliminary lemmas\<close>
 
 lemma Nil_genPrefix [iff]: "([], xs) : genPrefix r"
 by (cut_tac genPrefix.Nil [THEN genPrefix.append], auto)
@@ -84,7 +84,7 @@
 by (blast intro: genPrefix.prepend)
 
 
-subsection{*genPrefix is a partial order*}
+subsection\<open>genPrefix is a partial order\<close>
 
 lemma refl_genPrefix: "refl r ==> refl (genPrefix r)"
 apply (unfold refl_on_def, auto)
@@ -176,7 +176,7 @@
   by (blast intro: antisymI genPrefix_antisym)
 
 
-subsection{*recursion equations*}
+subsection\<open>recursion equations\<close>
 
 lemma genPrefix_Nil [simp]: "((xs, []) : genPrefix r) = (xs = [])"
   by (induct xs) auto
@@ -216,7 +216,7 @@
 apply (erule genPrefix.induct)
   apply blast
  apply simp
-txt{*Append case is hardest*}
+txt\<open>Append case is hardest\<close>
 apply simp
 apply (frule genPrefix_length_le [THEN le_imp_less_or_eq])
 apply (erule disjE)
@@ -258,7 +258,7 @@
 done
 
 
-subsection{*The type of lists is partially ordered*}
+subsection\<open>The type of lists is partially ordered\<close>
 
 declare refl_Id [iff] 
         antisym_Id [iff] 
@@ -376,7 +376,7 @@
   shows "xs <= zs \<Longrightarrow> ys <= zs \<Longrightarrow> xs <= ys | ys <= xs"
   by (induct zs rule: rev_induct) auto
 
-subsection{*pfixLe, pfixGe: properties inherited from the translations*}
+subsection\<open>pfixLe, pfixGe: properties inherited from the translations\<close>
 
 (** pfixLe **)
 
diff -r 703edebd1d92 -r f1ecba0272f9 src/HOL/UNITY/PPROD.thy
--- a/src/HOL/UNITY/PPROD.thy	Wed May 25 11:49:40 2016 +0200
+++ b/src/HOL/UNITY/PPROD.thy	Wed May 25 11:50:58 2016 +0200
@@ -68,7 +68,7 @@
     PLam I F \<in> transient A = (\<exists>i \<in> I. lift i (F i) \<in> transient A)"
 by (simp add: JN_transient PLam_def)
 
-text{*This holds because the @{term "F j"} cannot change @{term "lift_set i"}*}
+text\<open>This holds because the @{term "F j"} cannot change @{term "lift_set i"}\<close>
 lemma PLam_ensures:
      "[| i \<in> I;  F i \<in> (A \<times> UNIV) ensures (B \<times> UNIV);
          \<forall>j. F j \<in> preserves snd |]
@@ -114,11 +114,11 @@
 
 (*** guarantees properties ***)
 
-text{*This rule looks unsatisfactory because it refers to @{term lift}. 
+text\<open>This rule looks unsatisfactory because it refers to @{term lift}. 
   One must use
-  @{text lift_guarantees_eq_lift_inv} to rewrite the first subgoal and
-  something like @{text lift_preserves_sub} to rewrite the third.  However
-  there's no obvious alternative for the third premise.*}
+  \<open>lift_guarantees_eq_lift_inv\<close> to rewrite the first subgoal and
+  something like \<open>lift_preserves_sub\<close> to rewrite the third.  However
+  there's no obvious alternative for the third premise.\<close>
 lemma guarantees_PLam_I:
     "[| lift i (F i): X guarantees Y;  i \<in> I;
         OK I (%i. lift i (F i)) |]
diff -r 703edebd1d92 -r f1ecba0272f9 src/HOL/UNITY/ProgressSets.thy
--- a/src/HOL/UNITY/ProgressSets.thy	Wed May 25 11:49:40 2016 +0200
+++ b/src/HOL/UNITY/ProgressSets.thy	Wed May 25 11:50:58 2016 +0200
@@ -13,19 +13,19 @@
     Swiss Federal Institute of Technology Zurich (1997)
 *)
 
-section{*Progress Sets*}
+section\<open>Progress Sets\<close>
 
 theory ProgressSets imports Transformers begin
 
-subsection {*Complete Lattices and the Operator @{term cl}*}
+subsection \<open>Complete Lattices and the Operator @{term cl}\<close>
 
 definition lattice :: "'a set set => bool" where
-   --{*Meier calls them closure sets, but they are just complete lattices*}
+   \<comment>\<open>Meier calls them closure sets, but they are just complete lattices\<close>
    "lattice L ==
          (\<forall>M. M \<subseteq> L --> \<Inter>M \<in> L) & (\<forall>M. M \<subseteq> L --> \<Union>M \<in> L)"
 
 definition cl :: "['a set set, 'a set] => 'a set" where
-   --{*short for ``closure''*}
+   \<comment>\<open>short for ``closure''\<close>
    "cl L r == \<Inter>{x. x\<in>L & r \<subseteq> x}"
 
 lemma UNIV_in_lattice: "lattice L ==> UNIV \<in> L"
@@ -59,8 +59,8 @@
 lemma lattice_stable: "lattice {X. F \<in> stable X}"
 by (simp add: lattice_def stable_def constrains_def, blast)
 
-text{*The next three results state that @{term "cl L r"} is the minimal
- element of @{term L} that includes @{term r}.*}
+text\<open>The next three results state that @{term "cl L r"} is the minimal
+ element of @{term L} that includes @{term r}.\<close>
 lemma cl_in_lattice: "lattice L ==> cl L r \<in> L"
 apply (simp add: lattice_def cl_def)
 apply (erule conjE)  
@@ -70,18 +70,18 @@
 lemma cl_least: "[|c\<in>L; r\<subseteq>c|] ==> cl L r \<subseteq> c" 
 by (force simp add: cl_def)
 
-text{*The next three lemmas constitute assertion (4.61)*}
+text\<open>The next three lemmas constitute assertion (4.61)\<close>
 lemma cl_mono: "r \<subseteq> r' ==> cl L r \<subseteq> cl L r'"
 by (simp add: cl_def, blast)
 
 lemma subset_cl: "r \<subseteq> cl L r"
 by (simp add: cl_def le_Inf_iff)
 
-text{*A reformulation of @{thm subset_cl}*}
+text\<open>A reformulation of @{thm subset_cl}\<close>
 lemma clI: "x \<in> r ==> x \<in> cl L r"
 by (simp add: cl_def, blast)
 
-text{*A reformulation of @{thm cl_least}*}
+text\<open>A reformulation of @{thm cl_least}\<close>
 lemma clD: "[|c \<in> cl L r; B \<in> L; r \<subseteq> B|] ==> c \<in> B"
 by (force simp add: cl_def)
 
@@ -120,7 +120,7 @@
 lemma cl_UNIV [simp]: "lattice L ==> cl L UNIV = UNIV"
 by (simp add: cl_ident UNIV_in_lattice)
 
-text{*Assertion (4.62)*}
+text\<open>Assertion (4.62)\<close>
 lemma cl_ident_iff: "lattice L ==> (cl L r = r) = (r\<in>L)" 
 apply (rule iffI) 
  apply (erule subst)
@@ -132,9 +132,9 @@
 by (simp add: cl_ident_iff [symmetric] equalityI subset_cl)
 
 
-subsection {*Progress Sets and the Main Lemma*}
-text{*A progress set satisfies certain closure conditions and is a 
-simple way of including the set @{term "wens_set F B"}.*}
+subsection \<open>Progress Sets and the Main Lemma\<close>
+text\<open>A progress set satisfies certain closure conditions and is a 
+simple way of including the set @{term "wens_set F B"}.\<close>
 
 definition closed :: "['a program, 'a set, 'a set,  'a set set] => bool" where
    "closed F T B L == \<forall>M. \<forall>act \<in> Acts F. B\<subseteq>M & T\<inter>M \<in> L -->
@@ -149,15 +149,15 @@
     ==> T \<inter> (B \<union> wp act M) \<in> L" 
 by (simp add: closed_def) 
 
-text{*Note: the formalization below replaces Meier's @{term q} by @{term B}
-and @{term m} by @{term X}. *}
+text\<open>Note: the formalization below replaces Meier's @{term q} by @{term B}
+and @{term m} by @{term X}.\<close>
 
-text{*Part of the proof of the claim at the bottom of page 97.  It's
+text\<open>Part of the proof of the claim at the bottom of page 97.  It's
 proved separately because the argument requires a generalization over
-all @{term "act \<in> Acts F"}.*}
+all @{term "act \<in> Acts F"}.\<close>
 lemma lattice_awp_lemma:
-  assumes TXC:  "T\<inter>X \<in> C" --{*induction hypothesis in theorem below*}
-      and BsubX:  "B \<subseteq> X"   --{*holds in inductive step*}
+  assumes TXC:  "T\<inter>X \<in> C" \<comment>\<open>induction hypothesis in theorem below\<close>
+      and BsubX:  "B \<subseteq> X"   \<comment>\<open>holds in inductive step\<close>
       and latt: "lattice C"
       and TC:   "T \<in> C"
       and BC:   "B \<in> C"
@@ -173,10 +173,10 @@
 apply (blast intro: Un_in_lattice latt cl_in_lattice TXC) 
 done
 
-text{*Remainder of the proof of the claim at the bottom of page 97.*}
+text\<open>Remainder of the proof of the claim at the bottom of page 97.\<close>
 lemma lattice_lemma:
-  assumes TXC:  "T\<inter>X \<in> C" --{*induction hypothesis in theorem below*}
-      and BsubX:  "B \<subseteq> X"   --{*holds in inductive step*}
+  assumes TXC:  "T\<inter>X \<in> C" \<comment>\<open>induction hypothesis in theorem below\<close>
+      and BsubX:  "B \<subseteq> X"   \<comment>\<open>holds in inductive step\<close>
       and act:  "act \<in> Acts F"
       and latt: "lattice C"
       and TC:   "T \<in> C"
@@ -202,9 +202,9 @@
 done
 
 
-text{*Induction step for the main lemma*}
+text\<open>Induction step for the main lemma\<close>
 lemma progress_induction_step:
-  assumes TXC:  "T\<inter>X \<in> C" --{*induction hypothesis in theorem below*}
+  assumes TXC:  "T\<inter>X \<in> C" \<comment>\<open>induction hypothesis in theorem below\<close>
       and act:  "act \<in> Acts F"
       and Xwens: "X \<in> wens_set F B"
       and latt: "lattice C"
@@ -242,25 +242,25 @@
     by (rule cl_subset_in_lattice [OF cl_subset latt]) 
 qed
 
-text{*Proved on page 96 of Meier's thesis.  The special case when
+text\<open>Proved on page 96 of Meier's thesis.  The special case when
    @{term "T=UNIV"} states that every progress set for the program @{term F}
-   and set @{term B} includes the set @{term "wens_set F B"}.*}
+   and set @{term B} includes the set @{term "wens_set F B"}.\<close>
 lemma progress_set_lemma:
      "[|C \<in> progress_set F T B; r \<in> wens_set F B; F \<in> stable T|] ==> T\<inter>r \<in> C"
 apply (simp add: progress_set_def, clarify) 
 apply (erule wens_set.induct) 
-  txt{*Base*}
+  txt\<open>Base\<close>
   apply (simp add: Int_in_lattice) 
- txt{*The difficult @{term wens} case*}
+ txt\<open>The difficult @{term wens} case\<close>
  apply (simp add: progress_induction_step) 
-txt{*Disjunctive case*}
+txt\<open>Disjunctive case\<close>
 apply (subgoal_tac "(\<Union>U\<in>W. T \<inter> U) \<in> C") 
  apply simp 
 apply (blast intro: UN_in_lattice) 
 done
 
 
-subsection {*The Progress Set Union Theorem*}
+subsection \<open>The Progress Set Union Theorem\<close>
 
 lemma closed_mono:
   assumes BB':  "B \<subseteq> B'"
@@ -306,22 +306,22 @@
 done
 
 
-subsection {*Some Progress Sets*}
+subsection \<open>Some Progress Sets\<close>
 
 lemma UNIV_in_progress_set: "UNIV \<in> progress_set F T B"
 by (simp add: progress_set_def lattice_def closed_def)
 
 
 
-subsubsection {*Lattices and Relations*}
-text{*From Meier's thesis, section 4.5.3*}
+subsubsection \<open>Lattices and Relations\<close>
+text\<open>From Meier's thesis, section 4.5.3\<close>
 
 definition relcl :: "'a set set => ('a * 'a) set" where
-    -- {*Derived relation from a lattice*}
+    \<comment> \<open>Derived relation from a lattice\<close>
     "relcl L == {(x,y). y \<in> cl L {x}}"
   
 definition latticeof :: "('a * 'a) set => 'a set set" where
-    -- {*Derived lattice from a relation: the set of upwards-closed sets*}
+    \<comment> \<open>Derived lattice from a relation: the set of upwards-closed sets\<close>
     "latticeof r == {X. \<forall>s t. s \<in> X & (s,t) \<in> r --> t \<in> X}"
 
 
@@ -350,7 +350,7 @@
 apply (simp only: UN_in_lattice) 
 done
 
-text{*Equation (4.71) of Meier's thesis.  He gives no proof.*}
+text\<open>Equation (4.71) of Meier's thesis.  He gives no proof.\<close>
 lemma cl_latticeof:
      "[|refl r; trans r|] 
       ==> cl (latticeof r) X = {t. \<exists>s. s\<in>X & (s,t) \<in> r}" 
@@ -362,7 +362,7 @@
 apply (unfold cl_def, blast) 
 done
 
-text{*Related to (4.71).*}
+text\<open>Related to (4.71).\<close>
 lemma cl_eq_Collect_relcl:
      "lattice L ==> cl L X = {t. \<exists>s. s\<in>X & (s,t) \<in> relcl L}" 
 apply (cut_tac UN_singleton [of X]) 
@@ -370,7 +370,7 @@
 apply (force simp only: relcl_def cl_UN)
 done
 
-text{*Meier's theorem of section 4.5.3*}
+text\<open>Meier's theorem of section 4.5.3\<close>
 theorem latticeof_relcl_eq: "lattice L ==> latticeof (relcl L) = L"
 apply (rule equalityI) 
  prefer 2 apply (force simp add: latticeof_def relcl_def cl_def, clarify) 
@@ -394,14 +394,14 @@
 by (simp add: relcl_def cl_latticeof)
 
 
-subsubsection {*Decoupling Theorems*}
+subsubsection \<open>Decoupling Theorems\<close>
 
 definition decoupled :: "['a program, 'a program] => bool" where
    "decoupled F G ==
         \<forall>act \<in> Acts F. \<forall>B. G \<in> stable B --> G \<in> stable (wp act B)"
 
 
-text{*Rao's Decoupling Theorem*}
+text\<open>Rao's Decoupling Theorem\<close>
 lemma stableco: "F \<in> stable A ==> F \<in> A-B co A"
 by (simp add: stable_def constrains_def, blast) 
 
@@ -421,7 +421,7 @@
 qed
 
 
-text{*Rao's Weak Decoupling Theorem*}
+text\<open>Rao's Weak Decoupling Theorem\<close>
 theorem weak_decoupling:
   assumes leadsTo: "F \<in> A leadsTo B"
       and stable: "F\<squnion>G \<in> stable B"
@@ -439,12 +439,12 @@
   thus ?thesis by simp
 qed
 
-text{*The ``Decoupling via @{term G'} Union Theorem''*}
+text\<open>The ``Decoupling via @{term G'} Union Theorem''\<close>
 theorem decoupling_via_aux:
   assumes leadsTo: "F \<in> A leadsTo B"
       and prog: "{X. G' \<in> stable X} \<in> progress_set F UNIV B"
       and GG':  "G \<le> G'"  
-               --{*Beware!  This is the converse of the refinement relation!*}
+               \<comment>\<open>Beware!  This is the converse of the refinement relation!\<close>
   shows "F\<squnion>G \<in> A leadsTo B"
 proof -
   from prog have stable: "G' \<in> stable B"
@@ -456,16 +456,16 @@
 qed
 
 
-subsection{*Composition Theorems Based on Monotonicity and Commutativity*}
+subsection\<open>Composition Theorems Based on Monotonicity and Commutativity\<close>
 
-subsubsection{*Commutativity of @{term "cl L"} and assignment.*}
+subsubsection\<open>Commutativity of @{term "cl L"} and assignment.\<close>
 definition commutes :: "['a program, 'a set, 'a set,  'a set set] => bool" where
    "commutes F T B L ==
        \<forall>M. \<forall>act \<in> Acts F. B \<subseteq> M --> 
            cl L (T \<inter> wp act M) \<subseteq> T \<inter> (B \<union> wp act (cl L (T\<inter>M)))"
 
 
-text{*From Meier's thesis, section 4.5.6*}
+text\<open>From Meier's thesis, section 4.5.6\<close>
 lemma commutativity1_lemma:
   assumes commutes: "commutes F T B L" 
       and lattice:  "lattice L"
@@ -484,7 +484,7 @@
 apply (blast intro: rev_subsetD [OF _ wp_mono]) 
 done
 
-text{*Version packaged with @{thm progress_set_Union}*}
+text\<open>Version packaged with @{thm progress_set_Union}\<close>
 lemma commutativity1:
   assumes leadsTo: "F \<in> A leadsTo B"
       and lattice:  "lattice L"
@@ -499,7 +499,7 @@
 
 
 
-text{*Possibly move to Relation.thy, after @{term single_valued}*}
+text\<open>Possibly move to Relation.thy, after @{term single_valued}\<close>
 definition funof :: "[('a*'b)set, 'a] => 'b" where
    "funof r == (\<lambda>x. THE y. (x,y) \<in> r)"
 
@@ -518,11 +518,11 @@
 by (force simp add: in_wp_iff funof_eq)
 
 
-subsubsection{*Commutativity of Functions and Relation*}
-text{*Thesis, page 109*}
+subsubsection\<open>Commutativity of Functions and Relation\<close>
+text\<open>Thesis, page 109\<close>
 
 (*FIXME: this proof is still an ungodly mess*)
-text{*From Meier's thesis, section 4.5.6*}
+text\<open>From Meier's thesis, section 4.5.6\<close>
 lemma commutativity2_lemma:
   assumes dcommutes: 
       "\<And>act s t. act \<in> Acts F \<Longrightarrow> s \<in> T \<Longrightarrow> (s, t) \<in> relcl L \<Longrightarrow>
@@ -564,7 +564,7 @@
   then show "commutes F T B L" unfolding commutes_def by clarify
 qed
   
-text{*Version packaged with @{thm progress_set_Union}*}
+text\<open>Version packaged with @{thm progress_set_Union}\<close>
 lemma commutativity2:
   assumes leadsTo: "F \<in> A leadsTo B"
       and dcommutes: 
@@ -585,8 +585,8 @@
 done
 
 
-subsection {*Monotonicity*}
-text{*From Meier's thesis, section 4.5.7, page 110*}
+subsection \<open>Monotonicity\<close>
+text\<open>From Meier's thesis, section 4.5.7, page 110\<close>
 (*to be continued?*)
 
 end
diff -r 703edebd1d92 -r f1ecba0272f9 src/HOL/UNITY/Project.thy
--- a/src/HOL/UNITY/Project.thy	Wed May 25 11:49:40 2016 +0200
+++ b/src/HOL/UNITY/Project.thy	Wed May 25 11:50:58 2016 +0200
@@ -7,7 +7,7 @@
 Inheritance of GUARANTEES properties under extension.
 *)
 
-section{*Projections of State Sets*}
+section\<open>Projections of State Sets\<close>
 
 theory Project imports Extend begin
 
@@ -35,7 +35,7 @@
 done
 
 
-subsection{*Safety*}
+subsection\<open>Safety\<close>
 
 (*used below to prove Join_project_ensures*)
 lemma project_unless:
@@ -103,7 +103,7 @@
 end
 
 
-subsection{*"projecting" and union/intersection (no converses)*}
+subsection\<open>"projecting" and union/intersection (no converses)\<close>
 
 lemma projecting_Int: 
      "[| projecting C h F XA' XA;  projecting C h F XB' XB |]  
@@ -206,7 +206,7 @@
 by (force simp only: extending_def Join_project_increasing)
 
 
-subsection{*Reachability and project*}
+subsection\<open>Reachability and project\<close>
 
 (*In practice, C = reachable(...): the inclusion is equality*)
 lemma reachable_imp_reachable_project:
@@ -255,7 +255,7 @@
 done
 
 
-subsection{*Converse results for weak safety: benefits of the argument C *}
+subsection\<open>Converse results for weak safety: benefits of the argument C\<close>
 
 (*In practice, C = reachable(...): the inclusion is equality*)
 lemma reachable_project_imp_reachable:
@@ -337,8 +337,8 @@
 apply (simp (no_asm_simp) add: Increasing_def project_Stable extend_set_eq_Collect)
 done
 
-subsection{*A lot of redundant theorems: all are proved to facilitate reasoning
-    about guarantees.*}
+subsection\<open>A lot of redundant theorems: all are proved to facilitate reasoning
+    about guarantees.\<close>
 
 lemma projecting_Constrains: 
      "projecting (%G. reachable (extend h F\<squnion>G)) h F  
@@ -398,9 +398,9 @@
 done
 
 
-subsection{*leadsETo in the precondition (??)*}
+subsection\<open>leadsETo in the precondition (??)\<close>
 
-subsubsection{*transient*}
+subsubsection\<open>transient\<close>
 
 lemma transient_extend_set_imp_project_transient: 
      "[| G \<in> transient (C \<inter> extend_set h A);  G \<in> stable C |]   
@@ -424,7 +424,7 @@
 done
 
 
-subsubsection{*ensures -- a primitive combining progress with safety*}
+subsubsection\<open>ensures -- a primitive combining progress with safety\<close>
 
 (*Used to prove project_leadsETo_I*)
 lemma ensures_extend_set_imp_project_ensures:
@@ -458,7 +458,7 @@
                [THEN project_extend_transient_D, THEN transient_strengthen])
 done
 
-text{*Transferring a transient property upwards*}
+text\<open>Transferring a transient property upwards\<close>
 lemma project_transient_extend_set:
      "project h C G \<in> transient (project_set h C \<inter> A - B)
       ==> G \<in> transient (C \<inter> extend_set h A - extend_set h B)"
@@ -496,8 +496,8 @@
 apply (blast intro: project_transient_extend_set transient_strengthen)  
 done
 
-text{*Lemma useful for both STRONG and WEAK progress, but the transient
-    condition's very strong*}
+text\<open>Lemma useful for both STRONG and WEAK progress, but the transient
+    condition's very strong\<close>
 
 (*The strange induction formula allows induction over the leadsTo
   assumption's non-atomic precondition*)
@@ -528,7 +528,7 @@
                                   project_set_reachable_extend_eq)
 
 
-subsection{*Towards the theorem @{text project_Ensures_D}*}
+subsection\<open>Towards the theorem \<open>project_Ensures_D\<close>\<close>
 
 lemma project_ensures_D_lemma:
      "[| G \<in> stable ((C \<inter> extend_set h A) - (extend_set h B));   
@@ -566,7 +566,7 @@
 done
 
 
-subsection{*Guarantees*}
+subsection\<open>Guarantees\<close>
 
 lemma project_act_Restrict_subset_project_act:
      "project_act h (Restrict C act) \<subseteq> project_act h act"
@@ -618,9 +618,9 @@
 (*It seems that neither "guarantees" law can be proved from the other.*)
 
 
-subsection{*guarantees corollaries*}
+subsection\<open>guarantees corollaries\<close>
 
-subsubsection{*Some could be deleted: the required versions are easy to prove*}
+subsubsection\<open>Some could be deleted: the required versions are easy to prove\<close>
 
 lemma extend_guar_increasing:
      "[| F \<in> UNIV guarantees increasing func;   
@@ -651,7 +651,7 @@
 done
 
 
-subsubsection{*Guarantees with a leadsTo postcondition*}
+subsubsection\<open>Guarantees with a leadsTo postcondition\<close>
 
 lemma project_leadsTo_D:
      "F\<squnion>project h UNIV G \<in> A leadsTo B
diff -r 703edebd1d92 -r f1ecba0272f9 src/HOL/UNITY/Rename.thy
--- a/src/HOL/UNITY/Rename.thy	Wed May 25 11:49:40 2016 +0200
+++ b/src/HOL/UNITY/Rename.thy	Wed May 25 11:50:58 2016 +0200
@@ -3,7 +3,7 @@
     Copyright   2000  University of Cambridge
 *)
 
-section{*Renaming of State Sets*}
+section\<open>Renaming of State Sets\<close>
 
 theory Rename imports Extend begin
 
@@ -39,7 +39,7 @@
 by (simp add: rename_def)
 
 
-subsection{*inverse properties*}
+subsection\<open>inverse properties\<close>
 
 lemma extend_set_inv: 
      "bij h  
@@ -164,7 +164,7 @@
 by (blast intro: bij_rename bij_rename_imp_bij)
 
 
-subsection{*the lattice operations*}
+subsection\<open>the lattice operations\<close>
 
 lemma rename_SKIP [simp]: "bij h ==> rename h SKIP = SKIP"
 by (simp add: rename_def Extend.extend_SKIP)
@@ -178,7 +178,7 @@
 by (simp add: rename_def Extend.extend_JN)
 
 
-subsection{*Strong Safety: co, stable*}
+subsection\<open>Strong Safety: co, stable\<close>
 
 lemma rename_constrains: 
      "bij h ==> (rename h F \<in> (h`A) co (h`B)) = (F \<in> A co B)"
@@ -203,7 +203,7 @@
 done
 
 
-subsection{*Weak Safety: Co, Stable*}
+subsection\<open>Weak Safety: Co, Stable\<close>
 
 lemma reachable_rename_eq: 
      "bij h ==> reachable (rename h F) = h ` (reachable F)"
@@ -228,7 +228,7 @@
               bij_is_surj [THEN surj_f_inv_f])
 
 
-subsection{*Progress: transient, ensures*}
+subsection\<open>Progress: transient, ensures\<close>
 
 lemma rename_transient: 
      "bij h ==> (rename h F \<in> transient (h`A)) = (F \<in> transient A)"
@@ -288,7 +288,7 @@
 by (simp add: Extend.OK_extend_iff rename_def)
 
 
-subsection{*"image" versions of the rules, for lifting "guarantees" properties*}
+subsection\<open>"image" versions of the rules, for lifting "guarantees" properties\<close>
 
 (*All the proofs are similar.  Better would have been to prove one 
   meta-theorem, but how can we handle the polymorphism?  E.g. in 
diff -r 703edebd1d92 -r f1ecba0272f9 src/HOL/UNITY/Simple/Common.thy
--- a/src/HOL/UNITY/Simple/Common.thy	Wed May 25 11:49:40 2016 +0200
+++ b/src/HOL/UNITY/Simple/Common.thy	Wed May 25 11:50:58 2016 +0200
@@ -97,7 +97,7 @@
     then show ?case by simp
   qed
 next
-  from `n \<in> common`
+  from \<open>n \<in> common\<close>
   show "{..n} \<inter> id -` {n..} \<union> common \<subseteq> common"
     by (simp add: atMost_Int_atLeast)
 qed
diff -r 703edebd1d92 -r f1ecba0272f9 src/HOL/UNITY/Simple/Lift.thy
--- a/src/HOL/UNITY/Simple/Lift.thy	Wed May 25 11:49:40 2016 +0200
+++ b/src/HOL/UNITY/Simple/Lift.thy	Wed May 25 11:50:58 2016 +0200
@@ -10,21 +10,21 @@
 begin
 
 record state =
-  floor :: "int"            --{*current position of the lift*}
-  "open" :: "bool"          --{*whether the door is opened at floor*}
-  stop  :: "bool"           --{*whether the lift is stopped at floor*}
-  req   :: "int set"        --{*for each floor, whether the lift is requested*}
-  up    :: "bool"           --{*current direction of movement*}
-  move  :: "bool"           --{*whether moving takes precedence over opening*}
+  floor :: "int"            \<comment>\<open>current position of the lift\<close>
+  "open" :: "bool"          \<comment>\<open>whether the door is opened at floor\<close>
+  stop  :: "bool"           \<comment>\<open>whether the lift is stopped at floor\<close>
+  req   :: "int set"        \<comment>\<open>for each floor, whether the lift is requested\<close>
+  up    :: "bool"           \<comment>\<open>current direction of movement\<close>
+  move  :: "bool"           \<comment>\<open>whether moving takes precedence over opening\<close>
 
 axiomatization
-  Min :: "int" and   --{*least and greatest floors*}
-  Max :: "int"       --{*least and greatest floors*}
+  Min :: "int" and   \<comment>\<open>least and greatest floors\<close>
+  Max :: "int"       \<comment>\<open>least and greatest floors\<close>
 where
   Min_le_Max [iff]: "Min \<le> Max"
   
   
-  --{*Abbreviations: the "always" part*}
+  \<comment>\<open>Abbreviations: the "always" part\<close>
   
 definition
   above :: "state set"
@@ -50,7 +50,7 @@
   ready :: "state set"
   where "ready = {s. stop s & ~ open s & move s}"
  
-  --{*Further abbreviations*}
+  \<comment>\<open>Further abbreviations\<close>
 
 definition
   moving :: "state set"
@@ -65,7 +65,7 @@
   where "opened = {s. stop s  &  open s  &  move s}"
 
 definition
-  closed :: "state set"  --{*but this is the same as ready!!*}
+  closed :: "state set"  \<comment>\<open>but this is the same as ready!!\<close>
   where "closed = {s. stop s  & ~ open s &  move s}"
 
 definition
@@ -78,7 +78,7 @@
 
 
   
-  --{*The program*}
+  \<comment>\<open>The program\<close>
   
 definition
   request_act :: "(state*state) set"
@@ -128,12 +128,12 @@
 
 definition
   button_press  :: "(state*state) set"
-      --{*This action is omitted from prior treatments, which therefore are
+      \<comment>\<open>This action is omitted from prior treatments, which therefore are
         unrealistic: nobody asks the lift to do anything!  But adding this
         action invalidates many of the existing progress arguments: various
         "ensures" properties fail. Maybe it should be constrained to only
         allow button presses in the current direction of travel, like in a
-        real lift.*}
+        real lift.\<close>
   where "button_press =
          {(s,s'). \<exists>n. s' = s (|req := insert n (req s)|)
                         & Min \<le> n & n \<le> Max}"
@@ -141,7 +141,7 @@
 
 definition
   Lift :: "state program"
-    --{*for the moment, we OMIT @{text button_press}*}
+    \<comment>\<open>for the moment, we OMIT \<open>button_press\<close>\<close>
   where "Lift = mk_total_program
                 ({s. floor s = Min & ~ up s & move s & stop s &
                           ~ open s & req s = {}},
@@ -150,7 +150,7 @@
                  UNIV)"
 
 
-  --{*Invariants*}
+  \<comment>\<open>Invariants\<close>
 
 definition
   bounded :: "state set"
@@ -261,7 +261,7 @@
 done
 
 
-subsection{*Progress*}
+subsection\<open>Progress\<close>
 
 declare moving_def [THEN def_set_simp, simp]
 declare stopped_def [THEN def_set_simp, simp]
@@ -271,7 +271,7 @@
 declare Req_def [THEN def_set_simp, simp]
 
 
-text{*The HUG'93 paper mistakenly omits the Req n from these!*}
+text\<open>The HUG'93 paper mistakenly omits the Req n from these!\<close>
 
 (** Lift_1 **)
 lemma E_thm01: "Lift \<in> (stopped \<inter> atFloor n) LeadsTo (opened \<inter> atFloor n)"
diff -r 703edebd1d92 -r f1ecba0272f9 src/HOL/UNITY/Simple/NSP_Bad.thy
--- a/src/HOL/UNITY/Simple/NSP_Bad.thy	Wed May 25 11:49:40 2016 +0200
+++ b/src/HOL/UNITY/Simple/NSP_Bad.thy	Wed May 25 11:50:58 2016 +0200
@@ -5,15 +5,15 @@
 Original file is ../Auth/NS_Public_Bad
 *)
 
-section{*Analyzing the Needham-Schroeder Public-Key Protocol in UNITY*}
+section\<open>Analyzing the Needham-Schroeder Public-Key Protocol in UNITY\<close>
 
 theory NSP_Bad imports "../../Auth/Public" "../UNITY_Main" begin
 
-text{*This is the flawed version, vulnerable to Lowe's attack.
+text\<open>This is the flawed version, vulnerable to Lowe's attack.
 From page 260 of
   Burrows, Abadi and Needham.  A Logic of Authentication.
   Proc. Royal Soc. 426 (1989).
-*}
+\<close>
 
 type_synonym state = "event list"
 
@@ -63,8 +63,8 @@
 declare analz_into_parts [dest]
 declare Fake_parts_insert_in_Un  [dest]
 
-text{*For other theories, e.g. Mutex and Lift, using [iff] slows proofs down.
-  Here, it facilitates re-use of the Auth proofs.*}
+text\<open>For other theories, e.g. Mutex and Lift, using [iff] slows proofs down.
+  Here, it facilitates re-use of the Auth proofs.\<close>
 
 declare Fake_def [THEN def_act_simp, iff]
 declare NS1_def [THEN def_act_simp, iff]
@@ -74,8 +74,8 @@
 declare Nprg_def [THEN def_prg_Init, simp]
 
 
-text{*A "possibility property": there are traces that reach the end.
-  Replace by LEADSTO proof!*}
+text\<open>A "possibility property": there are traces that reach the end.
+  Replace by LEADSTO proof!\<close>
 lemma "A \<noteq> B ==>
        \<exists>NB. \<exists>s \<in> reachable Nprg. Says A B (Crypt (pubK B) (Nonce NB)) \<in> set s"
 apply (intro exI bexI)
@@ -88,7 +88,7 @@
 done
 
 
-subsection{*Inductive Proofs about @{term ns_public}*}
+subsection\<open>Inductive Proofs about @{term ns_public}\<close>
 
 lemma ns_constrainsI:
      "(!!act s s'. [| act \<in> {Id, Fake, NS1, NS2, NS3};
@@ -99,8 +99,8 @@
 done
 
 
-text{*This ML code does the inductions directly.*}
-ML{*
+text\<open>This ML code does the inductions directly.\<close>
+ML\<open>
 fun ns_constrains_tac ctxt i =
   SELECT_GOAL
     (EVERY
@@ -121,17 +121,17 @@
       (*"reachable" gets in here*)
       resolve_tac ctxt [@{thm Always_reachable} RS @{thm Always_ConstrainsI} RS @{thm StableI}] 1,
       ns_constrains_tac ctxt 1];
-*}
+\<close>
 
-method_setup ns_induct = {*
-    Scan.succeed (SIMPLE_METHOD' o ns_induct_tac) *}
+method_setup ns_induct = \<open>
+    Scan.succeed (SIMPLE_METHOD' o ns_induct_tac)\<close>
     "for inductive reasoning about the Needham-Schroeder protocol"
 
-text{*Converts invariants into statements about reachable states*}
+text\<open>Converts invariants into statements about reachable states\<close>
 lemmas Always_Collect_reachableD =
      Always_includes_reachable [THEN subsetD, THEN CollectD]
 
-text{*Spy never sees another agent's private key! (unless it's bad at start)*}
+text\<open>Spy never sees another agent's private key! (unless it's bad at start)\<close>
 lemma Spy_see_priK:
      "Nprg \<in> Always {s. (Key (priK A) \<in> parts (spies s)) = (A \<in> bad)}"
 apply ns_induct
@@ -145,10 +145,10 @@
 declare Spy_analz_priK [THEN Always_Collect_reachableD, simp]
 
 
-subsection{*Authenticity properties obtained from NS2*}
+subsection\<open>Authenticity properties obtained from NS2\<close>
 
-text{*It is impossible to re-use a nonce in both NS1 and NS2 provided the
-     nonce is secret.  (Honest users generate fresh nonces.)*}
+text\<open>It is impossible to re-use a nonce in both NS1 and NS2 provided the
+     nonce is secret.  (Honest users generate fresh nonces.)\<close>
 lemma no_nonce_NS1_NS2:
  "Nprg
   \<in> Always {s. Crypt (pubK C) \<lbrace>NA', Nonce NA\<rbrace> \<in> parts (spies s) -->
@@ -158,12 +158,12 @@
 apply (blast intro: analz_insertI)+
 done
 
-text{*Adding it to the claset slows down proofs...*}
+text\<open>Adding it to the claset slows down proofs...\<close>
 lemmas no_nonce_NS1_NS2_reachable =
        no_nonce_NS1_NS2 [THEN Always_Collect_reachableD, rule_format]
 
 
-text{*Unicity for NS1: nonce NA identifies agents A and B*}
+text\<open>Unicity for NS1: nonce NA identifies agents A and B\<close>
 lemma unique_NA_lemma:
      "Nprg
   \<in> Always {s. Nonce NA \<notin> analz (spies s) -->
@@ -172,10 +172,10 @@
                 A=A' & B=B'}"
 apply ns_induct
 apply auto
-txt{*Fake, NS1 are non-trivial*}
+txt\<open>Fake, NS1 are non-trivial\<close>
 done
 
-text{*Unicity for NS1: nonce NA identifies agents A and B*}
+text\<open>Unicity for NS1: nonce NA identifies agents A and B\<close>
 lemma unique_NA:
      "[| Crypt(pubK B)  \<lbrace>Nonce NA, Agent A\<rbrace> \<in> parts(spies s);
          Crypt(pubK B') \<lbrace>Nonce NA, Agent A'\<rbrace> \<in> parts(spies s);
@@ -185,26 +185,26 @@
 by (blast dest: unique_NA_lemma [THEN Always_Collect_reachableD])
 
 
-text{*Secrecy: Spy does not see the nonce sent in msg NS1 if A and B are secure*}
+text\<open>Secrecy: Spy does not see the nonce sent in msg NS1 if A and B are secure\<close>
 lemma Spy_not_see_NA:
      "[| A \<notin> bad;  B \<notin> bad |]
   ==> Nprg \<in> Always
               {s. Says A B (Crypt(pubK B) \<lbrace>Nonce NA, Agent A\<rbrace>) \<in> set s
                   --> Nonce NA \<notin> analz (spies s)}"
 apply ns_induct
-txt{*NS3*}
+txt\<open>NS3\<close>
 prefer 4 apply (blast intro: no_nonce_NS1_NS2_reachable)
-txt{*NS2*}
+txt\<open>NS2\<close>
 prefer 3 apply (blast dest: unique_NA)
-txt{*NS1*}
+txt\<open>NS1\<close>
 prefer 2 apply blast
-txt{*Fake*}
+txt\<open>Fake\<close>
 apply spy_analz
 done
 
 
-text{*Authentication for A: if she receives message 2 and has used NA
-  to start a run, then B has sent message 2.*}
+text\<open>Authentication for A: if she receives message 2 and has used NA
+  to start a run, then B has sent message 2.\<close>
 lemma A_trusts_NS2:
  "[| A \<notin> bad;  B \<notin> bad |]
   ==> Nprg \<in> Always
@@ -217,7 +217,7 @@
 done
 
 
-text{*If the encrypted message appears then it originated with Alice in NS1*}
+text\<open>If the encrypted message appears then it originated with Alice in NS1\<close>
 lemma B_trusts_NS1:
      "Nprg \<in> Always
               {s. Nonce NA \<notin> analz (spies s) -->
@@ -228,10 +228,10 @@
 done
 
 
-subsection{*Authenticity properties obtained from NS2*}
+subsection\<open>Authenticity properties obtained from NS2\<close>
 
-text{*Unicity for NS2: nonce NB identifies nonce NA and agent A.
-   Proof closely follows that of @{text unique_NA}.*}
+text\<open>Unicity for NS2: nonce NB identifies nonce NA and agent A.
+   Proof closely follows that of \<open>unique_NA\<close>.\<close>
 lemma unique_NB_lemma:
  "Nprg
   \<in> Always {s. Nonce NB \<notin> analz (spies s)  -->
@@ -240,7 +240,7 @@
                 A=A' & NA=NA'}"
 apply ns_induct
 apply auto
-txt{*Fake, NS2 are non-trivial*}
+txt\<open>Fake, NS2 are non-trivial\<close>
 done
 
 lemma unique_NB:
@@ -253,7 +253,7 @@
 done
 
 
-text{*NB remains secret PROVIDED Alice never responds with round 3*}
+text\<open>NB remains secret PROVIDED Alice never responds with round 3\<close>
 lemma Spy_not_see_NB:
      "[| A \<notin> bad;  B \<notin> bad |]
   ==> Nprg \<in> Always
@@ -262,20 +262,20 @@
                   --> Nonce NB \<notin> analz (spies s)}"
 apply ns_induct
 apply (simp_all (no_asm_simp) add: all_conj_distrib)
-txt{*NS3: because NB determines A*}
+txt\<open>NS3: because NB determines A\<close>
 prefer 4 apply (blast dest: unique_NB)
-txt{*NS2: by freshness and unicity of NB*}
+txt\<open>NS2: by freshness and unicity of NB\<close>
 prefer 3 apply (blast intro: no_nonce_NS1_NS2_reachable)
-txt{*NS1: by freshness*}
+txt\<open>NS1: by freshness\<close>
 prefer 2 apply blast
-txt{*Fake*}
+txt\<open>Fake\<close>
 apply spy_analz
 done
 
 
 
-text{*Authentication for B: if he receives message 3 and has used NB
-  in message 2, then A has sent message 3--to somebody....*}
+text\<open>Authentication for B: if he receives message 3 and has used NB
+  in message 2, then A has sent message 3--to somebody....\<close>
 lemma B_trusts_NS3:
      "[| A \<notin> bad;  B \<notin> bad |]
   ==> Nprg \<in> Always
@@ -286,29 +286,29 @@
 apply (insert Spy_not_see_NB [of A B NA NB], simp, ns_induct)
 apply (simp_all (no_asm_simp) add: ex_disj_distrib)
 apply auto
-txt{*NS3: because NB determines A. This use of @{text unique_NB} is robust.*}
+txt\<open>NS3: because NB determines A. This use of \<open>unique_NB\<close> is robust.\<close>
 apply (blast intro: unique_NB [THEN conjunct1])
 done
 
 
-text{*Can we strengthen the secrecy theorem?  NO*}
+text\<open>Can we strengthen the secrecy theorem?  NO\<close>
 lemma "[| A \<notin> bad;  B \<notin> bad |]
   ==> Nprg \<in> Always
               {s. Says B A (Crypt (pubK A) \<lbrace>Nonce NA, Nonce NB\<rbrace>) \<in> set s
                   --> Nonce NB \<notin> analz (spies s)}"
 apply ns_induct
 apply auto
-txt{*Fake*}
+txt\<open>Fake\<close>
 apply spy_analz
-txt{*NS2: by freshness and unicity of NB*}
+txt\<open>NS2: by freshness and unicity of NB\<close>
  apply (blast intro: no_nonce_NS1_NS2_reachable)
-txt{*NS3: unicity of NB identifies A and NA, but not B*}
+txt\<open>NS3: unicity of NB identifies A and NA, but not B\<close>
 apply (frule_tac A'=A in Says_imp_spies [THEN parts.Inj, THEN unique_NB])
 apply (erule Says_imp_spies [THEN parts.Inj], auto)
 apply (rename_tac s B' C)
-txt{*This is the attack!
+txt\<open>This is the attack!
 @{subgoals[display,indent=0,margin=65]}
-*}
+\<close>
 oops
 
 
diff -r 703edebd1d92 -r f1ecba0272f9 src/HOL/UNITY/Simple/Reach.thy
--- a/src/HOL/UNITY/Simple/Reach.thy	Wed May 25 11:49:40 2016 +0200
+++ b/src/HOL/UNITY/Simple/Reach.thy	Wed May 25 11:50:58 2016 +0200
@@ -33,7 +33,7 @@
   where "metric s = card {v. ~ s v}"
 
 
-text{**We assume that the set of vertices is finite*}
+text\<open>*We assume that the set of vertices is finite\<close>
 axiomatization where
   finite_graph:  "finite (UNIV :: vertex set)"
   
@@ -52,7 +52,7 @@
 
 declare asgt_def [THEN def_act_simp,simp]
 
-text{*All vertex sets are finite*}
+text\<open>All vertex sets are finite\<close>
 declare finite_subset [OF subset_UNIV finite_graph, iff]
 
 declare reach_invariant_def [THEN def_set_simp, simp]
diff -r 703edebd1d92 -r f1ecba0272f9 src/HOL/UNITY/Simple/Token.thy
--- a/src/HOL/UNITY/Simple/Token.thy	Wed May 25 11:49:40 2016 +0200
+++ b/src/HOL/UNITY/Simple/Token.thy	Wed May 25 11:50:58 2016 +0200
@@ -4,19 +4,19 @@
 *)
 
 
-section {*The Token Ring*}
+section \<open>The Token Ring\<close>
 
 theory Token
 imports "../WFair"
 
 begin
 
-text{*From Misra, "A Logic for Concurrent Programming" (1994), sections 5.2 and 13.2.*}
+text\<open>From Misra, "A Logic for Concurrent Programming" (1994), sections 5.2 and 13.2.\<close>
 
-subsection{*Definitions*}
+subsection\<open>Definitions\<close>
 
 datatype pstate = Hungry | Eating | Thinking
-    --{*process states*}
+    \<comment>\<open>process states\<close>
 
 record state =
   token :: "nat"
@@ -71,7 +71,7 @@
 done
 
 
-subsection{*Progress under Weak Fairness*}
+subsection\<open>Progress under Weak Fairness\<close>
 
 lemma wf_nodeOrder: "wf(nodeOrder j)"
 apply (unfold nodeOrder_def)
@@ -85,8 +85,8 @@
 apply (auto split add: nat_diff_split simp add: linorder_neq_iff mod_geq)
 done
 
-text{*From "A Logic for Concurrent Programming", but not used in Chapter 4.
-  Note the use of @{text cases}.  Reasoning about leadsTo takes practice!*}
+text\<open>From "A Logic for Concurrent Programming", but not used in Chapter 4.
+  Note the use of \<open>cases\<close>.  Reasoning about leadsTo takes practice!\<close>
 lemma TR7_nodeOrder:
      "[| i<N; j<N |] ==>    
       F \<in> (HasTok i) leadsTo ({s. (token s, i) \<in> nodeOrder j} \<union> HasTok j)"
@@ -97,7 +97,7 @@
 done
 
 
-text{*Chapter 4 variant, the one actually used below.*}
+text\<open>Chapter 4 variant, the one actually used below.\<close>
 lemma TR7_aux: "[| i<N; j<N; i\<noteq>j |]     
       ==> F \<in> (HasTok i) leadsTo {s. (token s, i) \<in> nodeOrder j}"
 apply (rule TR7 [THEN leadsTo_weaken_R])
@@ -109,7 +109,7 @@
 by auto
 
 
-text{*Misra's TR9: the token reaches an arbitrary node*}
+text\<open>Misra's TR9: the token reaches an arbitrary node\<close>
 lemma leadsTo_j: "j<N ==> F \<in> {s. token s < N} leadsTo (HasTok j)"
 apply (rule leadsTo_weaken_R)
 apply (rule_tac I = "-{j}" and f = token and B = "{}" 
@@ -121,7 +121,7 @@
 apply (auto simp add: HasTok_def nodeOrder_def)
 done
 
-text{*Misra's TR8: a hungry process eventually eats*}
+text\<open>Misra's TR8: a hungry process eventually eats\<close>
 lemma token_progress:
      "j<N ==> F \<in> ({s. token s < N} \<inter> H j) leadsTo (E j)"
 apply (rule leadsTo_cancel1 [THEN leadsTo_Un_duplicate])
diff -r 703edebd1d92 -r f1ecba0272f9 src/HOL/UNITY/SubstAx.thy
--- a/src/HOL/UNITY/SubstAx.thy	Wed May 25 11:49:40 2016 +0200
+++ b/src/HOL/UNITY/SubstAx.thy	Wed May 25 11:50:58 2016 +0200
@@ -5,7 +5,7 @@
 Weak LeadsTo relation (restricted to the set of reachable states)
 *)
 
-section{*Weak Progress*}
+section\<open>Weak Progress\<close>
 
 theory SubstAx imports WFair Constrains begin
 
@@ -18,7 +18,7 @@
 notation LeadsTo  (infixl "\<longmapsto>w" 60)
 
 
-text{*Resembles the previous definition of LeadsTo*}
+text\<open>Resembles the previous definition of LeadsTo\<close>
 lemma LeadsTo_eq_leadsTo: 
      "A LeadsTo B = {F. F \<in> (reachable F \<inter> A) leadsTo (reachable F \<inter> B)}"
 apply (unfold LeadsTo_def)
@@ -26,7 +26,7 @@
 done
 
 
-subsection{*Specialized laws for handling invariants*}
+subsection\<open>Specialized laws for handling invariants\<close>
 
 (** Conjoining an Always property **)
 
@@ -47,7 +47,7 @@
 lemmas Always_LeadsToD = Always_LeadsTo_post [THEN iffD2]
 
 
-subsection{*Introduction rules: Basis, Trans, Union*}
+subsection\<open>Introduction rules: Basis, Trans, Union\<close>
 
 lemma leadsTo_imp_LeadsTo: "F \<in> A leadsTo B ==> F \<in> A LeadsTo B"
 apply (simp add: LeadsTo_def)
@@ -68,12 +68,12 @@
 done
 
 
-subsection{*Derived rules*}
+subsection\<open>Derived rules\<close>
 
 lemma LeadsTo_UNIV [simp]: "F \<in> A LeadsTo UNIV"
 by (simp add: LeadsTo_def)
 
-text{*Useful with cancellation, disjunction*}
+text\<open>Useful with cancellation, disjunction\<close>
 lemma LeadsTo_Un_duplicate:
      "F \<in> A LeadsTo (A' \<union> A') ==> F \<in> A LeadsTo A'"
 by (simp add: Un_ac)
@@ -87,12 +87,12 @@
 apply (blast intro: LeadsTo_Union)
 done
 
-text{*Binary union introduction rule*}
+text\<open>Binary union introduction rule\<close>
 lemma LeadsTo_Un:
      "[| F \<in> A LeadsTo C; F \<in> B LeadsTo C |] ==> F \<in> (A \<union> B) LeadsTo C"
   using LeadsTo_UN [of "{A, B}" F id C] by auto
 
-text{*Lets us look at the starting state*}
+text\<open>Lets us look at the starting state\<close>
 lemma single_LeadsTo_I:
      "(!!s. s \<in> A ==> F \<in> {s} LeadsTo B) ==> F \<in> A LeadsTo B"
 by (subst UN_singleton [symmetric], rule LeadsTo_UN, blast)
@@ -176,8 +176,8 @@
 apply (blast intro: EnsuresI LeadsTo_Basis Always_ConstrainsD [THEN Constrains_weaken] transient_strengthen)
 done
 
-text{*Set difference: maybe combine with @{text leadsTo_weaken_L}??
-  This is the most useful form of the "disjunction" rule*}
+text\<open>Set difference: maybe combine with \<open>leadsTo_weaken_L\<close>??
+  This is the most useful form of the "disjunction" rule\<close>
 lemma LeadsTo_Diff:
      "[| F \<in> (A-B) LeadsTo C;  F \<in> (A \<inter> B) LeadsTo C |]  
       ==> F \<in> A LeadsTo C"
@@ -191,18 +191,18 @@
 done
 
 
-text{*Version with no index set*}
+text\<open>Version with no index set\<close>
 lemma LeadsTo_UN_UN_noindex: 
      "(!!i. F \<in> (A i) LeadsTo (A' i)) ==> F \<in> (\<Union>i. A i) LeadsTo (\<Union>i. A' i)"
 by (blast intro: LeadsTo_UN_UN)
 
-text{*Version with no index set*}
+text\<open>Version with no index set\<close>
 lemma all_LeadsTo_UN_UN:
      "\<forall>i. F \<in> (A i) LeadsTo (A' i)  
       ==> F \<in> (\<Union>i. A i) LeadsTo (\<Union>i. A' i)"
 by (blast intro: LeadsTo_UN_UN)
 
-text{*Binary union version*}
+text\<open>Binary union version\<close>
 lemma LeadsTo_Un_Un:
      "[| F \<in> A LeadsTo A'; F \<in> B LeadsTo B' |]  
             ==> F \<in> (A \<union> B) LeadsTo (A' \<union> B')"
@@ -240,18 +240,18 @@
 done
 
 
-text{*The impossibility law*}
+text\<open>The impossibility law\<close>
 
-text{*The set "A" may be non-empty, but it contains no reachable states*}
+text\<open>The set "A" may be non-empty, but it contains no reachable states\<close>
 lemma LeadsTo_empty: "[|F \<in> A LeadsTo {}; all_total F|] ==> F \<in> Always (-A)"
 apply (simp add: LeadsTo_def Always_eq_includes_reachable)
 apply (drule leadsTo_empty, auto)
 done
 
 
-subsection{*PSP: Progress-Safety-Progress*}
+subsection\<open>PSP: Progress-Safety-Progress\<close>
 
-text{*Special case of PSP: Misra's "stable conjunction"*}
+text\<open>Special case of PSP: Misra's "stable conjunction"\<close>
 lemma PSP_Stable:
      "[| F \<in> A LeadsTo A';  F \<in> Stable B |]  
       ==> F \<in> (A \<inter> B) LeadsTo (A' \<inter> B)"
@@ -298,7 +298,7 @@
 done
 
 
-subsection{*Induction rules*}
+subsection\<open>Induction rules\<close>
 
 (** Meta or object quantifier ????? **)
 lemma LeadsTo_wf_induct:
@@ -329,7 +329,7 @@
       ==> F \<in> A LeadsTo B"
 by (rule wf_less_than [THEN LeadsTo_wf_induct], auto)
 
-text{*Integer version.  Could generalize from 0 to any lower bound*}
+text\<open>Integer version.  Could generalize from 0 to any lower bound\<close>
 lemma integ_0_le_induct:
      "[| F \<in> Always {s. (0::int) \<le> f s};   
          !! z. F \<in> (A \<inter> {s. f s = z}) LeadsTo                      
@@ -363,7 +363,7 @@
 done
 
 
-subsection{*Completion: Binary and General Finite versions*}
+subsection\<open>Completion: Binary and General Finite versions\<close>
 
 lemma Completion:
      "[| F \<in> A LeadsTo (A' \<union> C);  F \<in> A' Co (A' \<union> C);  
diff -r 703edebd1d92 -r f1ecba0272f9 src/HOL/UNITY/Transformers.thy
--- a/src/HOL/UNITY/Transformers.thy	Wed May 25 11:49:40 2016 +0200
+++ b/src/HOL/UNITY/Transformers.thy	Wed May 25 11:50:58 2016 +0200
@@ -13,30 +13,30 @@
     Swiss Federal Institute of Technology Zurich (1997)
 *)
 
-section{*Predicate Transformers*}
+section\<open>Predicate Transformers\<close>
 
 theory Transformers imports Comp begin
 
-subsection{*Defining the Predicate Transformers @{term wp},
-   @{term awp} and  @{term wens}*}
+subsection\<open>Defining the Predicate Transformers @{term wp},
+   @{term awp} and  @{term wens}\<close>
 
 definition wp :: "[('a*'a) set, 'a set] => 'a set" where  
-    --{*Dijkstra's weakest-precondition operator (for an individual command)*}
+    \<comment>\<open>Dijkstra's weakest-precondition operator (for an individual command)\<close>
     "wp act B == - (act^-1 `` (-B))"
 
 definition awp :: "['a program, 'a set] => 'a set" where
-    --{*Dijkstra's weakest-precondition operator (for a program)*}
+    \<comment>\<open>Dijkstra's weakest-precondition operator (for a program)\<close>
     "awp F B == (\<Inter>act \<in> Acts F. wp act B)"
 
 definition wens :: "['a program, ('a*'a) set, 'a set] => 'a set" where
-    --{*The weakest-ensures transformer*}
+    \<comment>\<open>The weakest-ensures transformer\<close>
     "wens F act B == gfp(\<lambda>X. (wp act B \<inter> awp F (B \<union> X)) \<union> B)"
 
-text{*The fundamental theorem for wp*}
+text\<open>The fundamental theorem for wp\<close>
 theorem wp_iff: "(A <= wp act B) = (act `` A <= B)"
 by (force simp add: wp_def) 
 
-text{*This lemma is a good deal more intuitive than the definition!*}
+text\<open>This lemma is a good deal more intuitive than the definition!\<close>
 lemma in_wp_iff: "(a \<in> wp act B) = (\<forall>x. (a,x) \<in> act --> x \<in> B)"
 by (simp add: wp_def, blast)
 
@@ -46,7 +46,7 @@
 lemma wp_empty [simp]: "wp act {} = - (Domain act)"
 by (force simp add: wp_def)
 
-text{*The identity relation is the skip action*}
+text\<open>The identity relation is the skip action\<close>
 lemma wp_Id [simp]: "wp Id B = B"
 by (simp add: wp_def) 
 
@@ -60,7 +60,7 @@
 lemma awp_Int_eq: "awp F (A\<inter>B) = awp F A \<inter> awp F B"
 by (simp add: awp_def wp_def, blast) 
 
-text{*The fundamental theorem for awp*}
+text\<open>The fundamental theorem for awp\<close>
 theorem awp_iff_constrains: "(A <= awp F B) = (F \<in> A co B)"
 by (simp add: awp_def constrains_def wp_iff INT_subset_iff) 
 
@@ -88,8 +88,8 @@
 lemma wens_Id [simp]: "wens F Id B = B"
 by (simp add: wens_def gfp_def wp_def awp_def, blast)
 
-text{*These two theorems justify the claim that @{term wens} returns the
-weakest assertion satisfying the ensures property*}
+text\<open>These two theorems justify the claim that @{term wens} returns the
+weakest assertion satisfying the ensures property\<close>
 lemma ensures_imp_wens: "F \<in> A ensures B ==> \<exists>act \<in> Acts F. A \<subseteq> wens F act B"
 apply (simp add: wens_def ensures_def transient_def, clarify) 
 apply (rule rev_bexI, assumption) 
@@ -101,7 +101,7 @@
 by (simp add: wens_def gfp_def constrains_def awp_def wp_def
               ensures_def transient_def, blast)
 
-text{*These two results constitute assertion (4.13) of the thesis*}
+text\<open>These two results constitute assertion (4.13) of the thesis\<close>
 lemma wens_mono: "(A \<subseteq> B) ==> wens F act A \<subseteq> wens F act B"
 apply (simp add: wens_def wp_def awp_def) 
 apply (rule gfp_mono, blast) 
@@ -110,22 +110,22 @@
 lemma wens_weakening: "B \<subseteq> wens F act B"
 by (simp add: wens_def gfp_def, blast)
 
-text{*Assertion (6), or 4.16 in the thesis*}
+text\<open>Assertion (6), or 4.16 in the thesis\<close>
 lemma subset_wens: "A-B \<subseteq> wp act B \<inter> awp F (B \<union> A) ==> A \<subseteq> wens F act B" 
 apply (simp add: wens_def wp_def awp_def) 
 apply (rule gfp_upperbound, blast) 
 done
 
-text{*Assertion 4.17 in the thesis*}
+text\<open>Assertion 4.17 in the thesis\<close>
 lemma Diff_wens_constrains: "F \<in> (wens F act A - A) co wens F act A"
 by (simp add: wens_def gfp_def wp_def awp_def constrains_def, blast)
-  --{*Proved instantly, yet remarkably fragile. If @{text Un_subset_iff}
+  \<comment>\<open>Proved instantly, yet remarkably fragile. If \<open>Un_subset_iff\<close>
       is declared as an iff-rule, then it's almost impossible to prove. 
-      One proof is via @{text meson} after expanding all definitions, but it's
-      slow!*}
+      One proof is via \<open>meson\<close> after expanding all definitions, but it's
+      slow!\<close>
 
-text{*Assertion (7): 4.18 in the thesis.  NOTE that many of these results
-hold for an arbitrary action.  We often do not require @{term "act \<in> Acts F"}*}
+text\<open>Assertion (7): 4.18 in the thesis.  NOTE that many of these results
+hold for an arbitrary action.  We often do not require @{term "act \<in> Acts F"}\<close>
 lemma stable_wens: "F \<in> stable A ==> F \<in> stable (wens F act A)"
 apply (simp add: stable_def)
 apply (drule constrains_Un [OF Diff_wens_constrains [of F act A]]) 
@@ -134,7 +134,7 @@
 apply (simp add: wens_weakening)
 done
 
-text{*Assertion 4.20 in the thesis.*}
+text\<open>Assertion 4.20 in the thesis.\<close>
 lemma wens_Int_eq_lemma:
       "[|T-B \<subseteq> awp F T; act \<in> Acts F|]
        ==> T \<inter> wens F act B \<subseteq> wens F act (T\<inter>B)"
@@ -143,8 +143,8 @@
 apply (simp add: wp_def awp_def, blast)
 done
 
-text{*Assertion (8): 4.21 in the thesis. Here we indeed require
-      @{term "act \<in> Acts F"}*}
+text\<open>Assertion (8): 4.21 in the thesis. Here we indeed require
+      @{term "act \<in> Acts F"}\<close>
 lemma wens_Int_eq:
       "[|T-B \<subseteq> awp F T; act \<in> Acts F|]
        ==> T \<inter> wens F act B = T \<inter> wens F act (T\<inter>B)"
@@ -155,7 +155,7 @@
 done
 
 
-subsection{*Defining the Weakest Ensures Set*}
+subsection\<open>Defining the Weakest Ensures Set\<close>
 
 inductive_set
   wens_set :: "['a program, 'a set] => 'a set set"
@@ -198,29 +198,29 @@
 apply (blast intro: wens_set.Union) 
 done
 
-text{*Assertion (9): 4.27 in the thesis.*}
+text\<open>Assertion (9): 4.27 in the thesis.\<close>
 lemma leadsTo_iff_wens_set: "(F \<in> A leadsTo B) = (\<exists>C \<in> wens_set F B. A \<subseteq> C)"
 by (blast intro: leadsTo_imp_wens_set leadsTo_weaken_L wens_set_imp_leadsTo) 
 
-text{*This is the result that requires the definition of @{term wens_set} to
+text\<open>This is the result that requires the definition of @{term wens_set} to
   require @{term W} to be non-empty in the Unio case, for otherwise we should
-  always have @{term "{} \<in> wens_set F B"}.*}
+  always have @{term "{} \<in> wens_set F B"}.\<close>
 lemma wens_set_imp_subset: "A \<in> wens_set F B ==> B \<subseteq> A"
 apply (erule wens_set.induct) 
   apply (blast intro: wens_weakening [THEN subsetD])+
 done
 
 
-subsection{*Properties Involving Program Union*}
+subsection\<open>Properties Involving Program Union\<close>
 
-text{*Assertion (4.30) of thesis, reoriented*}
+text\<open>Assertion (4.30) of thesis, reoriented\<close>
 lemma awp_Join_eq: "awp (F\<squnion>G) B = awp F B \<inter> awp G B"
 by (simp add: awp_def wp_def, blast)
 
 lemma wens_subset: "wens F act B - B \<subseteq> wp act B \<inter> awp F (B \<union> wens F act B)"
 by (subst wens_unfold, fast) 
 
-text{*Assertion (4.31)*}
+text\<open>Assertion (4.31)\<close>
 lemma subset_wens_Join:
       "[|A = T \<inter> wens F act B;  T-B \<subseteq> awp F T; A-B \<subseteq> awp G (A \<union> B)|] 
        ==> A \<subseteq> wens (F\<squnion>G) act B"
@@ -232,14 +232,14 @@
 apply (insert wens_subset [of F act B], blast) 
 done
 
-text{*Assertion (4.32)*}
+text\<open>Assertion (4.32)\<close>
 lemma wens_Join_subset: "wens (F\<squnion>G) act B \<subseteq> wens F act B"
 apply (simp add: wens_def) 
 apply (rule gfp_mono)
 apply (auto simp add: awp_Join_eq)  
 done
 
-text{*Lemma, because the inductive step is just too messy.*}
+text\<open>Lemma, because the inductive step is just too messy.\<close>
 lemma wens_Union_inductive_step:
   assumes awpF: "T-B \<subseteq> awp F T"
       and awpG: "!!X. X \<in> wens_set F B ==> (T\<inter>X) - B \<subseteq> awp G (T\<inter>X)"
@@ -272,14 +272,14 @@
       and major: "X \<in> wens_set F B"
   shows "\<exists>Y \<in> wens_set (F\<squnion>G) B. Y \<subseteq> X & T\<inter>X = T\<inter>Y"
 apply (rule wens_set.induct [OF major])
-  txt{*Basis: trivial*}
+  txt\<open>Basis: trivial\<close>
   apply (blast intro: wens_set.Basis)
- txt{*Inductive step*}
+ txt\<open>Inductive step\<close>
  apply clarify 
  apply (rule_tac x = "wens (F\<squnion>G) act Y" in rev_bexI)
   apply (force intro: wens_set.Wens)
  apply (simp add: wens_Union_inductive_step [OF awpF awpG]) 
-txt{*Union: by Axiom of Choice*}
+txt\<open>Union: by Axiom of Choice\<close>
 apply (simp add: ball_conj_distrib Bex_def) 
 apply (clarify dest!: bchoice) 
 apply (rule_tac x = "\<Union>{Z. \<exists>U\<in>W. Z = f U}" in exI)
@@ -299,10 +299,10 @@
 done
 
 
-subsection {*The Set @{term "wens_set F B"} for a Single-Assignment Program*}
-text{*Thesis Section 4.3.3*}
+subsection \<open>The Set @{term "wens_set F B"} for a Single-Assignment Program\<close>
+text\<open>Thesis Section 4.3.3\<close>
 
-text{*We start by proving laws about single-assignment programs*}
+text\<open>We start by proving laws about single-assignment programs\<close>
 lemma awp_single_eq [simp]:
      "awp (mk_program (init, {act}, allowed)) B = B \<inter> wp act B"
 by (force simp add: awp_def wp_def) 
@@ -332,7 +332,7 @@
 by (simp add: wens_def gfp_def wp_def, blast)
 
 
-text{*Next, we express the @{term "wens_set"} for single-assignment programs*}
+text\<open>Next, we express the @{term "wens_set"} for single-assignment programs\<close>
 
 definition wens_single_finite :: "[('a*'a) set, 'a set, nat] => 'a set" where  
     "wens_single_finite act B k == \<Union>i \<in> atMost k. (wp act ^^ i) B"
@@ -416,7 +416,7 @@
 apply (simp add: atMost_Suc, blast)
 done
 
-text{*lemma for Union case*}
+text\<open>lemma for Union case\<close>
 lemma Union_eq_wens_single:
       "\<lbrakk>\<forall>k. \<not> W \<subseteq> wens_single_finite act B ` {..k};
         W \<subseteq> insert (wens_single act B)
@@ -439,15 +439,15 @@
            insert (wens_single act B) (range (wens_single_finite act B))"
 apply (rule subsetI)  
 apply (erule wens_set.induct)
-  txt{*Basis*} 
+  txt\<open>Basis\<close> 
   apply (fastforce simp add: wens_single_finite_def)
- txt{*Wens inductive step*}
+ txt\<open>Wens inductive step\<close>
  apply (case_tac "acta = Id", simp)
  apply (simp add: wens_single_eq)
  apply (elim disjE)
  apply (simp add: wens_single_Un_eq)
  apply (force simp add: wens_single_finite_Un_eq)
-txt{*Union inductive step*}
+txt\<open>Union inductive step\<close>
 apply (case_tac "\<exists>k. W \<subseteq> wens_single_finite act B ` (atMost k)")
  apply (blast dest!: subset_wens_single_finite, simp) 
 apply (rule disjI1 [OF Union_eq_wens_single], blast+)
@@ -471,7 +471,7 @@
 apply (blast intro: wens_set.Union wens_single_finite_in_wens_set)
 done
 
-text{*Theorem (4.29)*}
+text\<open>Theorem (4.29)\<close>
 theorem wens_set_single_eq:
      "[|F = mk_program (init, {act}, allowed); single_valued act|]
       ==> wens_set F B =
@@ -481,7 +481,7 @@
 apply (erule ssubst, erule single_subset_wens_set) 
 done
 
-text{*Generalizing Misra's Fixed Point Union Theorem (4.41)*}
+text\<open>Generalizing Misra's Fixed Point Union Theorem (4.41)\<close>
 
 lemma fp_leadsTo_Join:
     "[|T-B \<subseteq> awp F T; T-B \<subseteq> FP G; F \<in> A leadsTo B|] ==> F\<squnion>G \<in> T\<inter>A leadsTo B"
diff -r 703edebd1d92 -r f1ecba0272f9 src/HOL/UNITY/UNITY.thy
--- a/src/HOL/UNITY/UNITY.thy	Wed May 25 11:49:40 2016 +0200
+++ b/src/HOL/UNITY/UNITY.thy	Wed May 25 11:50:58 2016 +0200
@@ -8,7 +8,7 @@
 From Misra, "A Logic for Concurrent Programming", 1994.
 *)
 
-section {*The Basic UNITY Theory*}
+section \<open>The Basic UNITY Theory\<close>
 
 theory UNITY imports Main begin
 
@@ -54,11 +54,11 @@
     "invariant A == {F. Init F \<subseteq> A} \<inter> stable A"
 
 definition increasing :: "['a => 'b::{order}] => 'a program set" where
-    --{*Polymorphic in both states and the meaning of @{text "\<le>"}*}
+    \<comment>\<open>Polymorphic in both states and the meaning of \<open>\<le>\<close>\<close>
     "increasing f == \<Inter>z. stable {s. z \<le> f s}"
 
 
-subsubsection{*The abstract type of programs*}
+subsubsection\<open>The abstract type of programs\<close>
 
 lemmas program_typedef =
      Rep_Program Rep_Program_inverse Abs_Program_inverse 
@@ -83,7 +83,7 @@
 lemma insert_Id_AllowedActs [iff]: "insert Id (AllowedActs F) = AllowedActs F"
 by (simp add: insert_absorb)
 
-subsubsection{*Inspectors for type "program"*}
+subsubsection\<open>Inspectors for type "program"\<close>
 
 lemma Init_eq [simp]: "Init (mk_program (init,acts,allowed)) = init"
 by (simp add: program_typedef)
@@ -95,7 +95,7 @@
      "AllowedActs (mk_program (init,acts,allowed)) = insert Id allowed"
 by (simp add: program_typedef)
 
-subsubsection{*Equality for UNITY programs*}
+subsubsection\<open>Equality for UNITY programs\<close>
 
 lemma surjective_mk_program [simp]:
      "mk_program (Init F, Acts F, AllowedActs F) = F"
@@ -124,7 +124,7 @@
 by (blast intro: program_equalityI program_equalityE)
 
 
-subsubsection{*co*}
+subsubsection\<open>co\<close>
 
 lemma constrainsI: 
     "(!!act s s'. [| act: Acts F;  (s,s') \<in> act;  s \<in> A |] ==> s': A')  
@@ -147,12 +147,12 @@
 lemma constrains_UNIV2 [iff]: "F \<in> A co UNIV"
 by (unfold constrains_def, blast)
 
-text{*monotonic in 2nd argument*}
+text\<open>monotonic in 2nd argument\<close>
 lemma constrains_weaken_R: 
     "[| F \<in> A co A'; A'<=B' |] ==> F \<in> A co B'"
 by (unfold constrains_def, blast)
 
-text{*anti-monotonic in 1st argument*}
+text\<open>anti-monotonic in 1st argument\<close>
 lemma constrains_weaken_L: 
     "[| F \<in> A co A'; B \<subseteq> A |] ==> F \<in> B co A'"
 by (unfold constrains_def, blast)
@@ -161,7 +161,7 @@
    "[| F \<in> A co A'; B \<subseteq> A; A'<=B' |] ==> F \<in> B co B'"
 by (unfold constrains_def, blast)
 
-subsubsection{*Union*}
+subsubsection\<open>Union\<close>
 
 lemma constrains_Un: 
     "[| F \<in> A co A'; F \<in> B co B' |] ==> F \<in> (A \<union> B) co (A' \<union> B')"
@@ -184,7 +184,7 @@
 lemma constrains_INT_distrib: "A co (\<Inter>i \<in> I. B i) = (\<Inter>i \<in> I. A co B i)"
 by (unfold constrains_def, blast)
 
-subsubsection{*Intersection*}
+subsubsection\<open>Intersection\<close>
 
 lemma constrains_Int: 
     "[| F \<in> A co A'; F \<in> B co B' |] ==> F \<in> (A \<inter> B) co (A' \<inter> B')"
@@ -198,8 +198,8 @@
 lemma constrains_imp_subset: "F \<in> A co A' ==> A \<subseteq> A'"
 by (unfold constrains_def, auto)
 
-text{*The reasoning is by subsets since "co" refers to single actions
-  only.  So this rule isn't that useful.*}
+text\<open>The reasoning is by subsets since "co" refers to single actions
+  only.  So this rule isn't that useful.\<close>
 lemma constrains_trans: 
     "[| F \<in> A co B; F \<in> B co C |] ==> F \<in> A co C"
 by (unfold constrains_def, blast)
@@ -209,7 +209,7 @@
 by (unfold constrains_def, clarify, blast)
 
 
-subsubsection{*unless*}
+subsubsection\<open>unless\<close>
 
 lemma unlessI: "F \<in> (A-B) co (A \<union> B) ==> F \<in> A unless B"
 by (unfold unless_def, assumption)
@@ -218,7 +218,7 @@
 by (unfold unless_def, assumption)
 
 
-subsubsection{*stable*}
+subsubsection\<open>stable\<close>
 
 lemma stableI: "F \<in> A co A ==> F \<in> stable A"
 by (unfold stable_def, assumption)
@@ -229,7 +229,7 @@
 lemma stable_UNIV [simp]: "stable UNIV = UNIV"
 by (unfold stable_def constrains_def, auto)
 
-subsubsection{*Union*}
+subsubsection\<open>Union\<close>
 
 lemma stable_Un: 
     "[| F \<in> stable A; F \<in> stable A' |] ==> F \<in> stable (A \<union> A')"
@@ -248,7 +248,7 @@
     "(!!A. A \<in> X ==> F \<in> stable A) ==> F \<in> stable (\<Union>X)"
 by (unfold stable_def constrains_def, blast)
 
-subsubsection{*Intersection*}
+subsubsection\<open>Intersection\<close>
 
 lemma stable_Int: 
     "[| F \<in> stable A;  F \<in> stable A' |] ==> F \<in> stable (A \<inter> A')"
@@ -278,18 +278,18 @@
 lemmas stable_constrains_stable = stable_constrains_Int[THEN stableI]
 
 
-subsubsection{*invariant*}
+subsubsection\<open>invariant\<close>
 
 lemma invariantI: "[| Init F \<subseteq> A;  F \<in> stable A |] ==> F \<in> invariant A"
 by (simp add: invariant_def)
 
-text{*Could also say @{term "invariant A \<inter> invariant B \<subseteq> invariant(A \<inter> B)"}*}
+text\<open>Could also say @{term "invariant A \<inter> invariant B \<subseteq> invariant(A \<inter> B)"}\<close>
 lemma invariant_Int:
      "[| F \<in> invariant A;  F \<in> invariant B |] ==> F \<in> invariant (A \<inter> B)"
 by (auto simp add: invariant_def stable_Int)
 
 
-subsubsection{*increasing*}
+subsubsection\<open>increasing\<close>
 
 lemma increasingD: 
      "F \<in> increasing f ==> F \<in> stable {s. z \<subseteq> f s}"
@@ -319,15 +319,15 @@
      ==> F \<in> {s. s x \<in> M} co (\<Union>m \<in> M. B m)"
 by (unfold constrains_def, blast)
 
-text{*As above, but for the trivial case of a one-variable state, in which the
-  state is identified with its one variable.*}
+text\<open>As above, but for the trivial case of a one-variable state, in which the
+  state is identified with its one variable.\<close>
 lemma elimination_sing: 
     "(\<forall>m \<in> M. F \<in> {m} co (B m)) ==> F \<in> M co (\<Union>m \<in> M. B m)"
 by (unfold constrains_def, blast)
 
 
 
-subsubsection{*Theoretical Results from Section 6*}
+subsubsection\<open>Theoretical Results from Section 6\<close>
 
 lemma constrains_strongest_rhs: 
     "F \<in> A co (strongest_rhs F A )"
@@ -338,7 +338,7 @@
 by (unfold constrains_def strongest_rhs_def, blast)
 
 
-subsubsection{*Ad-hoc set-theory rules*}
+subsubsection\<open>Ad-hoc set-theory rules\<close>
 
 lemma Un_Diff_Diff [simp]: "A \<union> B - (A - B) = B"
 by blast
@@ -346,7 +346,7 @@
 lemma Int_Union_Union: "\<Union>B \<inter> A = \<Union>((%C. C \<inter> A)`B)"
 by blast
 
-text{*Needed for WF reasoning in WFair.thy*}
+text\<open>Needed for WF reasoning in WFair.thy\<close>
 
 lemma Image_less_than [simp]: "less_than `` {k} = greaterThan k"
 by blast
@@ -355,7 +355,7 @@
 by blast
 
 
-subsection{*Partial versus Total Transitions*}
+subsection\<open>Partial versus Total Transitions\<close>
 
 definition totalize_act :: "('a * 'a)set => ('a * 'a)set" where
     "totalize_act act == act \<union> Id_on (-(Domain act))"
@@ -376,7 +376,7 @@
 by (blast intro: sym [THEN image_eqI])
 
 
-subsubsection{*Basic properties*}
+subsubsection\<open>Basic properties\<close>
 
 lemma totalize_act_Id [simp]: "totalize_act Id = Id"
 by (simp add: totalize_act_def) 
@@ -427,9 +427,9 @@
 by (simp add: mk_total_program_def)
 
 
-subsection{*Rules for Lazy Definition Expansion*}
+subsection\<open>Rules for Lazy Definition Expansion\<close>
 
-text{*They avoid expanding the full program, which is a large expression*}
+text\<open>They avoid expanding the full program, which is a large expression\<close>
 
 lemma def_prg_Init:
      "F = mk_total_program (init,acts,allowed) ==> Init F = init"
@@ -445,16 +445,16 @@
       ==> AllowedActs F = insert Id allowed"
 by (simp add: mk_total_program_def)
 
-text{*An action is expanded if a pair of states is being tested against it*}
+text\<open>An action is expanded if a pair of states is being tested against it\<close>
 lemma def_act_simp:
      "act = {(s,s'). P s s'} ==> ((s,s') \<in> act) = P s s'"
 by (simp add: mk_total_program_def)
 
-text{*A set is expanded only if an element is being tested against it*}
+text\<open>A set is expanded only if an element is being tested against it\<close>
 lemma def_set_simp: "A = B ==> (x \<in> A) = (x \<in> B)"
 by (simp add: mk_total_program_def)
 
-subsubsection{*Inspectors for type "program"*}
+subsubsection\<open>Inspectors for type "program"\<close>
 
 lemma Init_total_eq [simp]:
      "Init (mk_total_program (init,acts,allowed)) = init"
diff -r 703edebd1d92 -r f1ecba0272f9 src/HOL/UNITY/UNITY_Main.thy
--- a/src/HOL/UNITY/UNITY_Main.thy	Wed May 25 11:49:40 2016 +0200
+++ b/src/HOL/UNITY/UNITY_Main.thy	Wed May 25 11:50:58 2016 +0200
@@ -3,7 +3,7 @@
     Copyright   2003  University of Cambridge
 *)
 
-section{*Comprehensive UNITY Theory*}
+section\<open>Comprehensive UNITY Theory\<close>
 
 theory UNITY_Main
 imports Detects PPROD Follows ProgressSets
@@ -11,19 +11,19 @@
 
 ML_file "UNITY_tactics.ML"
 
-method_setup safety = {*
-    Scan.succeed (SIMPLE_METHOD' o constrains_tac) *}
+method_setup safety = \<open>
+    Scan.succeed (SIMPLE_METHOD' o constrains_tac)\<close>
     "for proving safety properties"
 
-method_setup ensures_tac = {*
+method_setup ensures_tac = \<open>
   Args.goal_spec -- Scan.lift Args.embedded_inner_syntax >>
   (fn (quant, s) => fn ctxt => SIMPLE_METHOD'' quant (ensures_tac ctxt s))
-*} "for proving progress properties"
+\<close> "for proving progress properties"
 
-setup {*
+setup \<open>
   map_theory_simpset (fn ctxt => ctxt
     addsimps (make_o_equivs ctxt @{thm fst_o_funPair} @ make_o_equivs ctxt @{thm snd_o_funPair})
     addsimps (make_o_equivs ctxt @{thm fst_o_lift_map} @ make_o_equivs ctxt @{thm snd_o_lift_map}))
-*}
+\<close>
 
 end
diff -r 703edebd1d92 -r f1ecba0272f9 src/HOL/UNITY/Union.thy
--- a/src/HOL/UNITY/Union.thy	Wed May 25 11:49:40 2016 +0200
+++ b/src/HOL/UNITY/Union.thy	Wed May 25 11:50:58 2016 +0200
@@ -5,7 +5,7 @@
 Partly from Misra's Chapter 5: Asynchronous Compositions of Programs.
 *)
 
-section{*Unions of Programs*}
+section\<open>Unions of Programs\<close>
 
 theory Union imports SubstAx FP begin
 
@@ -47,7 +47,7 @@
   "\<Squnion>x. B" == "CONST JOIN (CONST UNIV) (\<lambda>x. B)"
 
 
-subsection{*SKIP*}
+subsection\<open>SKIP\<close>
 
 lemma Init_SKIP [simp]: "Init SKIP = UNIV"
 by (simp add: SKIP_def)
@@ -61,7 +61,7 @@
 lemma reachable_SKIP [simp]: "reachable SKIP = UNIV"
 by (force elim: reachable.induct intro: reachable.intros)
 
-subsection{*SKIP and safety properties*}
+subsection\<open>SKIP and safety properties\<close>
 
 lemma SKIP_in_constrains_iff [iff]: "(SKIP \<in> A co B) = (A \<subseteq> B)"
 by (unfold constrains_def, auto)
@@ -75,7 +75,7 @@
 declare SKIP_in_stable [THEN stable_imp_Stable, iff]
 
 
-subsection{*Join*}
+subsection\<open>Join\<close>
 
 lemma Init_Join [simp]: "Init (F\<squnion>G) = Init F \<inter> Init G"
 by (simp add: Join_def)
@@ -88,7 +88,7 @@
 by (auto simp add: Join_def)
 
 
-subsection{*JN*}
+subsection\<open>JN\<close>
 
 lemma JN_empty [simp]: "(\<Squnion>i\<in>{}. F i) = SKIP"
 by (unfold JOIN_def SKIP_def, auto)
@@ -114,7 +114,7 @@
 by (simp add: JOIN_def)
 
 
-subsection{*Algebraic laws*}
+subsection\<open>Algebraic laws\<close>
 
 lemma Join_commute: "F\<squnion>G = G\<squnion>F"
 by (simp add: Join_def Un_commute Int_commute)
@@ -151,7 +151,7 @@
 lemmas Join_ac = Join_assoc Join_left_absorb Join_commute Join_left_commute
 
 
-subsection{*Laws Governing @{text "\<Squnion>"}*}
+subsection\<open>Laws Governing \<open>\<Squnion>\<close>\<close>
 
 (*Also follows by JN_insert and insert_absorb, but the proof is longer*)
 lemma JN_absorb: "k \<in> I ==> F k\<squnion>(\<Squnion>i \<in> I. F i) = (\<Squnion>i \<in> I. F i)"
@@ -178,7 +178,7 @@
 done
 
 
-subsection{*Safety: co, stable, FP*}
+subsection\<open>Safety: co, stable, FP\<close>
 
 (*Fails if I={} because it collapses to SKIP \<in> A co B, i.e. to A \<subseteq> B.  So an
   alternative precondition is A \<subseteq> B, but most proofs using this rule require
@@ -240,7 +240,7 @@
 by (simp add: FP_def JN_stable INTER_eq)
 
 
-subsection{*Progress: transient, ensures*}
+subsection\<open>Progress: transient, ensures\<close>
 
 lemma JN_transient:
      "i \<in> I ==>  
@@ -308,7 +308,7 @@
 done
 
 
-subsection{*the ok and OK relations*}
+subsection\<open>the ok and OK relations\<close>
 
 lemma ok_SKIP1 [iff]: "SKIP ok F"
 by (simp add: ok_def)
@@ -355,7 +355,7 @@
 by (auto simp add: OK_iff_ok)
 
 
-subsection{*Allowed*}
+subsection\<open>Allowed\<close>
 
 lemma Allowed_SKIP [simp]: "Allowed SKIP = UNIV"
 by (auto simp add: Allowed_def)
@@ -372,8 +372,8 @@
 lemma OK_iff_Allowed: "OK I F = (\<forall>i \<in> I. \<forall>j \<in> I-{i}. F i \<in> Allowed(F j))"
 by (auto simp add: OK_iff_ok ok_iff_Allowed)
 
-subsection{*@{term safety_prop}, for reasoning about
- given instances of "ok"*}
+subsection\<open>@{term safety_prop}, for reasoning about
+ given instances of "ok"\<close>
 
 lemma safety_prop_Acts_iff:
      "safety_prop X ==> (Acts G \<subseteq> insert Id (UNION X Acts)) = (G \<in> X)"
@@ -418,7 +418,7 @@
   moreover assume "Acts G \<subseteq> (\<Union>j\<in>\<Inter>i\<in>I. X i. Acts j)"
   ultimately have "Acts G \<subseteq> (\<Union>i\<in>X i. Acts i)"
     by auto
-  with * `i \<in> I` show "G \<in> X i" by blast
+  with * \<open>i \<in> I\<close> show "G \<in> X i" by blast
 qed
 
 lemma safety_prop_INTER1 [simp]:
@@ -443,7 +443,7 @@
       ==> F ok G = (G \<in> X & acts \<subseteq> AllowedActs G)"
 by (auto simp add: ok_def safety_prop_Acts_iff)
 
-text{*The union of two total programs is total.*}
+text\<open>The union of two total programs is total.\<close>
 lemma totalize_Join: "totalize F\<squnion>totalize G = totalize (F\<squnion>G)"
 by (simp add: program_equalityI totalize_def Join_def image_Un)
 
diff -r 703edebd1d92 -r f1ecba0272f9 src/HOL/UNITY/WFair.thy
--- a/src/HOL/UNITY/WFair.thy	Wed May 25 11:49:40 2016 +0200
+++ b/src/HOL/UNITY/WFair.thy	Wed May 25 11:50:58 2016 +0200
@@ -7,11 +7,11 @@
 From Misra, "A Logic for Concurrent Programming", 1994
 *)
 
-section{*Progress*}
+section\<open>Progress\<close>
 
 theory WFair imports UNITY begin
 
-text{*The original version of this theory was based on weak fairness.  (Thus,
+text\<open>The original version of this theory was based on weak fairness.  (Thus,
 the entire UNITY development embodied this assumption, until February 2003.)
 Weak fairness states that if a command is enabled continuously, then it is
 eventually executed.  Ernie Cohen suggested that I instead adopt unconditional
@@ -30,14 +30,14 @@
 property, it simplifies many proofs.  A drawback is that some laws only hold
 under the assumption that all transitions are total.  The best-known of these
 is the impossibility law for leads-to.
-*}
+\<close>
 
 definition
 
-  --{*This definition specifies conditional fairness.  The rest of the theory
+  \<comment>\<open>This definition specifies conditional fairness.  The rest of the theory
       is generic to all forms of fairness.  To get weak fairness, conjoin
       the inclusion below with @{term "A \<subseteq> Domain act"}, which specifies 
-      that the action is enabled over all of @{term A}.*}
+      that the action is enabled over all of @{term A}.\<close>
   transient :: "'a set => 'a program set" where
     "transient A == {F. \<exists>act\<in>Acts F. act``A \<subseteq> -A}"
 
@@ -48,7 +48,7 @@
 
 inductive_set
   leads :: "'a program => ('a set * 'a set) set"
-    --{*LEADS-TO constant for the inductive definition*}
+    \<comment>\<open>LEADS-TO constant for the inductive definition\<close>
   for F :: "'a program"
   where
 
@@ -60,17 +60,17 @@
 
 
 definition leadsTo :: "['a set, 'a set] => 'a program set" (infixl "leadsTo" 60) where
-     --{*visible version of the LEADS-TO relation*}
+     \<comment>\<open>visible version of the LEADS-TO relation\<close>
     "A leadsTo B == {F. (A,B) \<in> leads F}"
   
 definition wlt :: "['a program, 'a set] => 'a set" where
-     --{*predicate transformer: the largest set that leads to @{term B}*}
+     \<comment>\<open>predicate transformer: the largest set that leads to @{term B}\<close>
     "wlt F B == \<Union>{A. F \<in> A leadsTo B}"
 
 notation leadsTo  (infixl "\<longmapsto>" 60)
 
 
-subsection{*transient*}
+subsection\<open>transient\<close>
 
 lemma stable_transient: 
     "[| F \<in> stable A; F \<in> transient A |] ==> \<exists>act\<in>Acts F. A \<subseteq> - (Domain act)"
@@ -104,9 +104,9 @@
 by (unfold transient_def, auto)
 
 
-text{*This equation recovers the notion of weak fairness.  A totalized
+text\<open>This equation recovers the notion of weak fairness.  A totalized
       program satisfies a transient assertion just if the original program
-      contains a suitable action that is also enabled.*}
+      contains a suitable action that is also enabled.\<close>
 lemma totalize_transient_iff:
    "(totalize F \<in> transient A) = (\<exists>act\<in>Acts F. A \<subseteq> Domain act & act``A \<subseteq> -A)"
 apply (simp add: totalize_def totalize_act_def transient_def 
@@ -119,7 +119,7 @@
      ==> totalize F \<in> transient A"
 by (simp add: totalize_transient_iff, blast)
 
-subsection{*ensures*}
+subsection\<open>ensures\<close>
 
 lemma ensuresI: 
     "[| F \<in> (A-B) co (A \<union> B); F \<in> transient (A-B) |] ==> F \<in> A ensures B"
@@ -135,7 +135,7 @@
 apply (blast intro: constrains_weaken transient_strengthen)
 done
 
-text{*The L-version (precondition strengthening) fails, but we have this*}
+text\<open>The L-version (precondition strengthening) fails, but we have this\<close>
 lemma stable_ensures_Int: 
     "[| F \<in> stable C;  F \<in> A ensures B |]    
     ==> F \<in> (C \<inter> A) ensures (C \<inter> B)"
@@ -155,7 +155,7 @@
 by (simp (no_asm) add: ensures_def unless_def)
 
 
-subsection{*leadsTo*}
+subsection\<open>leadsTo\<close>
 
 lemma leadsTo_Basis [intro]: "F \<in> A ensures B ==> F \<in> A leadsTo B"
 apply (unfold leadsTo_def)
@@ -179,7 +179,7 @@
 lemma transient_imp_leadsTo: "F \<in> transient A ==> F \<in> A leadsTo (-A)"
 by (simp (no_asm_simp) add: leadsTo_Basis ensuresI Compl_partition)
 
-text{*Useful with cancellation, disjunction*}
+text\<open>Useful with cancellation, disjunction\<close>
 lemma leadsTo_Un_duplicate: "F \<in> A leadsTo (A' \<union> A') ==> F \<in> A leadsTo A'"
 by (simp add: Un_ac)
 
@@ -187,7 +187,7 @@
      "F \<in> A leadsTo (A' \<union> C \<union> C) ==> F \<in> A leadsTo (A' \<union> C)"
 by (simp add: Un_ac)
 
-text{*The Union introduction rule as we should have liked to state it*}
+text\<open>The Union introduction rule as we should have liked to state it\<close>
 lemma leadsTo_Union: 
     "(!!A. A \<in> S ==> F \<in> A leadsTo B) ==> F \<in> (\<Union>S) leadsTo B"
 apply (unfold leadsTo_def)
@@ -206,7 +206,7 @@
 apply (blast intro: leadsTo_Union)
 done
 
-text{*Binary union introduction rule*}
+text\<open>Binary union introduction rule\<close>
 lemma leadsTo_Un:
      "[| F \<in> A leadsTo C; F \<in> B leadsTo C |] ==> F \<in> (A \<union> B) leadsTo C"
   using leadsTo_Union [of "{A, B}" F C] by auto
@@ -216,7 +216,7 @@
 by (subst UN_singleton [symmetric], rule leadsTo_UN, blast)
 
 
-text{*The INDUCTION rule as we should have liked to state it*}
+text\<open>The INDUCTION rule as we should have liked to state it\<close>
 lemma leadsTo_induct: 
   "[| F \<in> za leadsTo zb;   
       !!A B. F \<in> A ensures B ==> P A B;  
@@ -245,16 +245,16 @@
 
 (** Variant induction rule: on the preconditions for B **)
 
-text{*Lemma is the weak version: can't see how to do it in one step*}
+text\<open>Lemma is the weak version: can't see how to do it in one step\<close>
 lemma leadsTo_induct_pre_lemma: 
   "[| F \<in> za leadsTo zb;   
       P zb;  
       !!A B. [| F \<in> A ensures B;  P B |] ==> P A;  
       !!S. \<forall>A \<in> S. P A ==> P (\<Union>S)  
    |] ==> P za"
-txt{*by induction on this formula*}
+txt\<open>by induction on this formula\<close>
 apply (subgoal_tac "P zb --> P za")
-txt{*now solve first subgoal: this formula is sufficient*}
+txt\<open>now solve first subgoal: this formula is sufficient\<close>
 apply (blast intro: leadsTo_refl)
 apply (erule leadsTo_induct)
 apply (blast+)
@@ -282,7 +282,7 @@
      "[| F \<in> A leadsTo A'; B \<subseteq> A |] ==> F \<in> B leadsTo A'"
 by (blast intro: leadsTo_Trans subset_imp_leadsTo)
 
-text{*Distributes over binary unions*}
+text\<open>Distributes over binary unions\<close>
 lemma leadsTo_Un_distrib:
      "F \<in> (A \<union> B) leadsTo C  =  (F \<in> A leadsTo C & F \<in> B leadsTo C)"
 by (blast intro: leadsTo_Un leadsTo_weaken_L)
@@ -301,7 +301,7 @@
 by (blast intro: leadsTo_weaken_R leadsTo_weaken_L leadsTo_Trans)
 
 
-text{*Set difference: maybe combine with @{text leadsTo_weaken_L}??*}
+text\<open>Set difference: maybe combine with \<open>leadsTo_weaken_L\<close>??\<close>
 lemma leadsTo_Diff:
      "[| F \<in> (A-B) leadsTo C; F \<in> B leadsTo C |]   ==> F \<in> A leadsTo C"
 by (blast intro: leadsTo_Un leadsTo_weaken)
@@ -312,7 +312,7 @@
 apply (blast intro: leadsTo_Union leadsTo_weaken_R)
 done
 
-text{*Binary union version*}
+text\<open>Binary union version\<close>
 lemma leadsTo_Un_Un:
      "[| F \<in> A leadsTo A'; F \<in> B leadsTo B' |]  
       ==> F \<in> (A \<union> B) leadsTo (A' \<union> B')"
@@ -350,7 +350,7 @@
 done
 
 
-text{*The impossibility law*}
+text\<open>The impossibility law\<close>
 lemma leadsTo_empty: "[|F \<in> A leadsTo {}; all_total F|] ==> A={}"
 apply (erule leadsTo_induct_pre)
 apply (simp_all add: ensures_def constrains_def transient_def all_total_def, clarify)
@@ -358,9 +358,9 @@
 apply blast
 done
 
-subsection{*PSP: Progress-Safety-Progress*}
+subsection\<open>PSP: Progress-Safety-Progress\<close>
 
-text{*Special case of PSP: Misra's "stable conjunction"*}
+text\<open>Special case of PSP: Misra's "stable conjunction"\<close>
 lemma psp_stable: 
    "[| F \<in> A leadsTo A'; F \<in> stable B |]  
     ==> F \<in> (A \<inter> B) leadsTo (A' \<inter> B)"
@@ -389,9 +389,9 @@
       ==> F \<in> (A \<inter> B') leadsTo ((A' \<inter> B) \<union> (B' - B))"
 apply (erule leadsTo_induct)
   prefer 3 apply (blast intro: leadsTo_Union_Int)
- txt{*Basis case*}
+ txt\<open>Basis case\<close>
  apply (blast intro: psp_ensures)
-txt{*Transitivity case has a delicate argument involving "cancellation"*}
+txt\<open>Transitivity case has a delicate argument involving "cancellation"\<close>
 apply (rule leadsTo_Un_duplicate2)
 apply (erule leadsTo_cancel_Diff1)
 apply (simp add: Int_Diff Diff_triv)
@@ -413,7 +413,7 @@
 done
 
 
-subsection{*Proving the induction rules*}
+subsection\<open>Proving the induction rules\<close>
 
 (** The most general rule: r is any wf relation; f is any variant function **)
 
@@ -490,9 +490,9 @@
 done
 
 
-subsection{*wlt*}
+subsection\<open>wlt\<close>
 
-text{*Misra's property W3*}
+text\<open>Misra's property W3\<close>
 lemma wlt_leadsTo: "F \<in> (wlt F B) leadsTo B"
 apply (unfold wlt_def)
 apply (blast intro!: leadsTo_Union)
@@ -503,17 +503,17 @@
 apply (blast intro!: leadsTo_Union)
 done
 
-text{*Misra's property W2*}
+text\<open>Misra's property W2\<close>
 lemma leadsTo_eq_subset_wlt: "F \<in> A leadsTo B = (A \<subseteq> wlt F B)"
 by (blast intro!: leadsTo_subset wlt_leadsTo [THEN leadsTo_weaken_L])
 
-text{*Misra's property W4*}
+text\<open>Misra's property W4\<close>
 lemma wlt_increasing: "B \<subseteq> wlt F B"
 apply (simp (no_asm_simp) add: leadsTo_eq_subset_wlt [symmetric] subset_imp_leadsTo)
 done
 
 
-text{*Used in the Trans case below*}
+text\<open>Used in the Trans case below\<close>
 lemma lemma1: 
    "[| B \<subseteq> A2;   
        F \<in> (A1 - B) co (A1 \<union> B);  
@@ -521,18 +521,18 @@
     ==> F \<in> (A1 \<union> A2 - C) co (A1 \<union> A2 \<union> C)"
 by (unfold constrains_def, clarify,  blast)
 
-text{*Lemma (1,2,3) of Misra's draft book, Chapter 4, "Progress"*}
+text\<open>Lemma (1,2,3) of Misra's draft book, Chapter 4, "Progress"\<close>
 lemma leadsTo_123:
      "F \<in> A leadsTo A'  
       ==> \<exists>B. A \<subseteq> B & F \<in> B leadsTo A' & F \<in> (B-A') co (B \<union> A')"
 apply (erule leadsTo_induct)
-  txt{*Basis*}
+  txt\<open>Basis\<close>
   apply (blast dest: ensuresD)
- txt{*Trans*}
+ txt\<open>Trans\<close>
  apply clarify
  apply (rule_tac x = "Ba \<union> Bb" in exI)
  apply (blast intro: lemma1 leadsTo_Un_Un leadsTo_cancel1 leadsTo_Un_duplicate)
-txt{*Union*}
+txt\<open>Union\<close>
 apply (clarify dest!: ball_conj_distrib [THEN iffD1] bchoice)
 apply (rule_tac x = "\<Union>A \<in> S. f A" in exI)
 apply (auto intro: leadsTo_UN)
@@ -542,7 +542,7 @@
 done
 
 
-text{*Misra's property W5*}
+text\<open>Misra's property W5\<close>
 lemma wlt_constrains_wlt: "F \<in> (wlt F B - B) co (wlt F B)"
 proof -
   from wlt_leadsTo [of F B, THEN leadsTo_123]
@@ -564,7 +564,7 @@
 qed
 
 
-subsection{*Completion: Binary and General Finite versions*}
+subsection\<open>Completion: Binary and General Finite versions\<close>
 
 lemma completion_lemma :
      "[| W = wlt F (B' \<union> C);