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)"