diff -r c8a2755bf220 -r ff784d5a5bfb src/HOL/Unix/Nested_Environment.thy
--- a/src/HOL/Unix/Nested_Environment.thy	Sat Jan 05 17:00:43 2019 +0100
+++ b/src/HOL/Unix/Nested_Environment.thy	Sat Jan 05 17:24:33 2019 +0100
@@ -10,8 +10,8 @@
 
 text \<open>
   Consider a partial function @{term [source] "e :: 'a \<Rightarrow> 'b option"}; this may
-  be understood as an \<^emph>\<open>environment\<close> mapping indexes @{typ 'a} to optional
-  entry values @{typ 'b} (cf.\ the basic theory \<open>Map\<close> of Isabelle/HOL). This
+  be understood as an \<^emph>\<open>environment\<close> mapping indexes \<^typ>\<open>'a\<close> to optional
+  entry values \<^typ>\<open>'b\<close> (cf.\ the basic theory \<open>Map\<close> of Isabelle/HOL). This
   basic idea is easily generalized to that of a \<^emph>\<open>nested environment\<close>, where
   entries may be either basic values or again proper environments. Then each
   entry is accessed by a \<^emph>\<open>path\<close>, i.e.\ a list of indexes leading to its
@@ -24,9 +24,9 @@
 
 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
+  In the type \<^typ>\<open>('a, 'b, 'c) env\<close> the parameter \<^typ>\<open>'a\<close> refers to
+  basic values (occurring in terminal positions), type \<^typ>\<open>'b\<close> to values
+  associated with proper (inner) environments, and type \<^typ>\<open>'c\<close> 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.
@@ -39,7 +39,7 @@
   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>\<open>defined position\<close> within a nested environment is one where
-  @{term lookup} at its path does not yield @{term None}.
+  \<^term>\<open>lookup\<close> at its path does not yield \<^term>\<open>None\<close>.
 \<close>
 
 primrec lookup :: "('a, 'b, 'c) env \<Rightarrow> 'c list \<Rightarrow> ('a, 'b, 'c) env option"
@@ -57,7 +57,7 @@
 
 text \<open>
   \<^medskip>
-  The characteristic cases of @{term lookup} are expressed by the following
+  The characteristic cases of \<^term>\<open>lookup\<close> are expressed by the following
   equalities.
 \<close>
 
@@ -92,7 +92,7 @@
 
 text \<open>
   \<^medskip>
-  Displaced @{term lookup} operations, relative to a certain base path prefix,
+  Displaced \<^term>\<open>lookup\<close> 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>
@@ -178,7 +178,7 @@
 
 text \<open>
   \<^medskip>
-  Successful @{term lookup} deeper down an environment structure means we are
+  Successful \<^term>\<open>lookup\<close> 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>
@@ -194,8 +194,7 @@
 qed
 
 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
+  The subsequent statement describes in more detail how a successful \<^term>\<open>lookup\<close> with a non-empty path results in a certain situation at any upper
   position.
 \<close>
 
@@ -265,7 +264,7 @@
 
 text \<open>
   \<^medskip>
-  The characteristic cases of @{term update} are expressed by the following
+  The characteristic cases of \<^term>\<open>update\<close> are expressed by the following
   equalities.
 \<close>
 
@@ -316,8 +315,8 @@
 
 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}
+  The most basic correspondence of \<^term>\<open>lookup\<close> and \<^term>\<open>update\<close> states
+  that after \<^term>\<open>update\<close> at a defined position, subsequent \<^term>\<open>lookup\<close>
   operations would yield the new value.
 \<close>
 
@@ -364,10 +363,9 @@
 
 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.
+  The properties of displaced \<^term>\<open>update\<close> operations are analogous to those
+  of \<^term>\<open>lookup\<close> above. There are two cases: below an undefined position
+  \<^term>\<open>update\<close> is absorbed altogether, and below a defined positions \<^term>\<open>update\<close> affects subsequent \<^term>\<open>lookup\<close> operations in the obvious way.
 \<close>
 
 theorem update_append_none:
@@ -459,9 +457,8 @@
 
 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.
+  Apparently, \<^term>\<open>update\<close> does not affect the result of subsequent \<^term>\<open>lookup\<close> operations at independent positions, i.e.\ in case that the paths
+  for \<^term>\<open>update\<close> and \<^term>\<open>lookup\<close> fork at a certain point.
 \<close>
 
 theorem lookup_update_other: