diff -r dbe216a75a4b -r 4a16f8e41879 src/HOL/Unix/Nested_Environment.thy
--- a/src/HOL/Unix/Nested_Environment.thy	Tue Oct 07 20:34:17 2014 +0200
+++ b/src/HOL/Unix/Nested_Environment.thy	Tue Oct 07 20:43:18 2014 +0200
@@ -2,13 +2,13 @@
     Author:     Markus Wenzel, TU Muenchen
 *)
 
-header {* Nested environments *}
+header \<open>Nested environments\<close>
 
 theory Nested_Environment
 imports Main
 begin
 
-text {*
+text \<open>
   Consider a partial function @{term [source] "e :: 'a \<Rightarrow> 'b option"};
   this may be understood as an \emph{environment} mapping indexes
   @{typ 'a} to optional entry values @{typ 'b} (cf.\ the basic theory
@@ -17,31 +17,31 @@
   basic values or again proper environments.  Then each entry is
   accessed by a \emph{path}, i.e.\ a list of indexes leading to its
   position within the structure.
-*}
+\<close>
 
 datatype (dead 'a, dead 'b, dead 'c) env =
     Val 'a
   | Env 'b  "'c \<Rightarrow> ('a, 'b, 'c) env option"
 
-text {*
+text \<open>
   \medskip In the type @{typ "('a, 'b, 'c) env"} the parameter @{typ
   'a} refers to basic values (occurring in terminal positions), type
   @{typ 'b} to values associated with proper (inner) environments, and
   type @{typ 'c} with the index type for branching.  Note that there
   is no restriction on any of these types.  In particular, arbitrary
   branching may yield rather large (transfinite) tree structures.
-*}
+\<close>
 
 
-subsection {* The lookup operation *}
+subsection \<open>The lookup operation\<close>
 
-text {*
+text \<open>
   Lookup in nested environments works by following a given path of
   index elements, leading to an optional result (a terminal value or
   nested environment).  A \emph{defined position} within a nested
   environment is one where @{term lookup} at its path does not yield
   @{term None}.
-*}
+\<close>
 
 primrec lookup :: "('a, 'b, 'c) env \<Rightarrow> 'c list \<Rightarrow> ('a, 'b, 'c) env option"
   and lookup_option :: "('a, 'b, 'c) env option \<Rightarrow> 'c list \<Rightarrow> ('a, 'b, 'c) env option"
@@ -56,10 +56,10 @@
 
 hide_const lookup_option
 
-text {*
+text \<open>
   \medskip The characteristic cases of @{term lookup} are expressed by
   the following equalities.
-*}
+\<close>
 
 theorem lookup_nil: "lookup e [] = Some e"
   by (cases e) simp_all
@@ -90,12 +90,12 @@
           | Some e \<Rightarrow> lookup e xs)))"
   by (simp split: list.split env.split)
 
-text {*
+text \<open>
   \medskip Displaced @{term lookup} operations, relative to a certain
   base path prefix, may be reduced as follows.  There are two cases,
   depending whether the environment actually extends far enough to
   follow the base path.
-*}
+\<close>
 
 theorem lookup_append_none:
   assumes "lookup env xs = None"
@@ -119,7 +119,7 @@
       with Env show ?thesis by simp
     next
       case (Some e)
-      note es = `es x = Some e`
+      note es = \<open>es x = Some e\<close>
       show ?thesis
       proof (cases "lookup e xs")
         case None
@@ -144,7 +144,7 @@
   then show "lookup env ([] @ ys) = lookup e ys" by simp
 next
   case (Cons x xs)
-  note asm = `lookup env (x # xs) = Some e`
+  note asm = \<open>lookup env (x # xs) = Some e\<close>
   show "lookup env ((x # xs) @ ys) = lookup e ys"
   proof (cases env)
     case (Val a)
@@ -159,7 +159,7 @@
       then show ?thesis ..
     next
       case (Some e')
-      note es = `es x = Some e'`
+      note es = \<open>es x = Some e'\<close>
       show ?thesis
       proof (cases "lookup e' xs")
         case None
@@ -176,12 +176,12 @@
   qed
 qed
 
-text {*
+text \<open>
   \medskip Successful @{term lookup} deeper down an environment
   structure means we are able to peek further up as well.  Note that
   this is basically just the contrapositive statement of @{thm
   [source] lookup_append_none} above.
-*}
+\<close>
 
 theorem lookup_some_append:
   assumes "lookup env (xs @ ys) = Some e"
@@ -193,11 +193,11 @@
   then show ?thesis by (simp)
 qed
 
-text {*
+text \<open>
   The subsequent statement describes in more detail how a successful
   @{term lookup} with a non-empty path results in a certain situation
   at any upper position.
-*}
+\<close>
 
 theorem lookup_some_upper:
   assumes "lookup env (xs @ y # ys) = Some e"
@@ -236,14 +236,14 @@
 qed
 
 
-subsection {* The update operation *}
+subsection \<open>The update operation\<close>
 
-text {*
+text \<open>
   Update at a certain position in a nested environment may either
   delete an existing entry, or overwrite an existing one.  Note that
   update at undefined positions is simple absorbed, i.e.\ the
   environment is left unchanged.
-*}
+\<close>
 
 primrec update :: "'c list \<Rightarrow> ('a, 'b, 'c) env option \<Rightarrow>
     ('a, 'b, 'c) env \<Rightarrow> ('a, 'b, 'c) env"
@@ -264,10 +264,10 @@
 
 hide_const update_option
 
-text {*
+text \<open>
   \medskip The characteristic cases of @{term update} are expressed by
   the following equalities.
-*}
+\<close>
 
 theorem update_nil_none: "update [] None env = env"
   by (cases env) simp_all
@@ -314,11 +314,11 @@
                   | Some e \<Rightarrow> Some (update (y # ys) opt e)))))))"
   by (simp split: list.split env.split option.split)
 
-text {*
+text \<open>
   \medskip The most basic correspondence of @{term lookup} and @{term
   update} states that after @{term update} at a defined position,
   subsequent @{term lookup} operations would yield the new value.
-*}
+\<close>
 
 theorem lookup_update_some:
   assumes "lookup env xs = Some e"
@@ -331,7 +331,7 @@
 next
   case (Cons x xs)
   note hyp = Cons.hyps
-    and asm = `lookup env (x # xs) = Some e`
+    and asm = \<open>lookup env (x # xs) = Some e\<close>
   show ?case
   proof (cases env)
     case (Val a)
@@ -346,7 +346,7 @@
       then show ?thesis ..
     next
       case (Some e')
-      note es = `es x = Some e'`
+      note es = \<open>es x = Some e'\<close>
       show ?thesis
       proof (cases xs)
         case Nil
@@ -361,13 +361,13 @@
   qed
 qed
 
-text {*
+text \<open>
   \medskip The properties of displaced @{term update} operations are
   analogous to those of @{term lookup} above.  There are two cases:
   below an undefined position @{term update} is absorbed altogether,
   and below a defined positions @{term update} affects subsequent
   @{term lookup} operations in the obvious way.
-*}
+\<close>
 
 theorem update_append_none:
   assumes "lookup env xs = None"
@@ -380,7 +380,7 @@
 next
   case (Cons x xs)
   note hyp = Cons.hyps
-    and asm = `lookup env (x # xs) = None`
+    and asm = \<open>lookup env (x # xs) = None\<close>
   show "update ((x # xs) @ y # ys) opt env = env"
   proof (cases env)
     case (Val a)
@@ -390,12 +390,12 @@
     show ?thesis
     proof (cases "es x")
       case None
-      note es = `es x = None`
+      note es = \<open>es x = None\<close>
       show ?thesis
         by (cases xs) (simp_all add: es Env fun_upd_idem_iff)
     next
       case (Some e)
-      note es = `es x = Some e`
+      note es = \<open>es x = Some e\<close>
       show ?thesis
       proof (cases xs)
         case Nil
@@ -423,7 +423,7 @@
 next
   case (Cons x xs)
   note hyp = Cons.hyps
-    and asm = `lookup env (x # xs) = Some e`
+    and asm = \<open>lookup env (x # xs) = Some e\<close>
   show "lookup (update ((x # xs) @ y # ys) opt env) (x # xs) =
       Some (update (y # ys) opt e)"
   proof (cases env)
@@ -439,7 +439,7 @@
       then show ?thesis ..
     next
       case (Some e')
-      note es = `es x = Some e'`
+      note es = \<open>es x = Some e'\<close>
       show ?thesis
       proof (cases xs)
         case Nil
@@ -456,12 +456,12 @@
   qed
 qed
 
-text {*
+text \<open>
   \medskip Apparently, @{term update} does not affect the result of
   subsequent @{term lookup} operations at independent positions, i.e.\
   in case that the paths for @{term update} and @{term lookup} fork at
   a certain point.
-*}
+\<close>
 
 theorem lookup_update_other:
   assumes neq: "y \<noteq> (z::'c)"
@@ -519,7 +519,7 @@
 qed
 
 
-subsection {* Code generation *}
+subsection \<open>Code generation\<close>
 
 lemma [code, code del]:
   "(HOL.equal :: (_, _, _) env \<Rightarrow> _) = HOL.equal" ..
@@ -549,7 +549,7 @@
     show ?lhs
     proof
       fix z
-      from `?rhs` have "?prop z" ..
+      from \<open>?rhs\<close> have "?prop z" ..
       then show "f z = g z" by (auto split: option.splits)
     qed
   qed