
diff -r 6e2479089226 -r cecd7a941885 ProgTutorial/Essential.thy
--- a/ProgTutorial/Essential.thy	Tue May 14 16:59:53 2019 +0200
+++ b/ProgTutorial/Essential.thy	Tue May 14 17:10:47 2019 +0200
@@ -2,9 +2,9 @@
 imports Base First_Steps
 begin
 
-chapter {* Isabelle Essentials *}
-
-text {*
+chapter \<open>Isabelle Essentials\<close>
+
+text \<open>
    \begin{flushright}
   {\em One man's obfuscation is another man's abstraction.} \\[1ex]
   Frank Ch.~Eigler on the Linux Kernel Mailing List,\\ 
@@ -17,15 +17,15 @@
   is a small trusted core and everything else is built on top of this trusted
   core. The fundamental data structures involved in this core are certified
   terms and certified types, as well as theorems.
-*}
-
-
-section {* Terms and Types *}
-
-text {*
+\<close>
+
+
+section \<open>Terms and Types\<close>
+
+text \<open>
   In Isabelle, there are certified terms and uncertified terms (respectively types). 
   Uncertified terms are often just called terms. One way to construct them is by 
-  using the antiquotation \mbox{@{text "@{term \<dots>}"}}. For example
+  using the antiquotation \mbox{\<open>@{term \<dots>}\<close>}. For example
 
   @{ML_response [display,gray] 
 "@{term \"(a::nat) + b = c\"}" 
@@ -35,17 +35,17 @@
   constructs the term @{term "(a::nat) + b = c"}. The resulting term is printed using 
   the internal representation corresponding to the datatype @{ML_type_ind "term"}, 
   which is defined as follows: 
-*}  
-
-ML_val %linenosgray{*datatype term =
+\<close>  
+
+ML_val %linenosgray\<open>datatype term =
   Const of string * typ 
 | Free of string * typ 
 | Var of indexname * typ 
 | Bound of int 
 | Abs of string * typ * term 
-| $ of term * term *}
-
-text {*
+| $ of term * term\<close>
+
+text \<open>
   This datatype implements Church-style lambda-terms, where types are
   explicitly recorded in variables, constants and abstractions.  The
   important point of having terms is that you can pattern-match against them;
@@ -127,8 +127,8 @@
 
   When constructing terms, you are usually concerned with free
   variables (as mentioned earlier, you cannot construct schematic
-  variables using the built-in antiquotation \mbox{@{text "@{term
-  \<dots>}"}}). If you deal with theorems, you have to, however, observe the
+  variables using the built-in antiquotation \mbox{\<open>@{term
+  \<dots>}\<close>}). If you deal with theorems, you have to, however, observe the
   distinction. The reason is that only schematic variables can be
   instantiated with terms when a theorem is applied. A similar
   distinction between free and schematic variables holds for types
@@ -177,13 +177,13 @@
   may omit parts of it by default. If you want to see all of it, you
   need to set the printing depth to a higher value by 
   \end{exercise}
-*}
+\<close>
 
 declare [[ML_print_depth = 50]]
 
-text {*
-  The antiquotation @{text "@{prop \<dots>}"} constructs terms by inserting the 
-  usually invisible @{text "Trueprop"}-coercions whenever necessary. 
+text \<open>
+  The antiquotation \<open>@{prop \<dots>}\<close> constructs terms by inserting the 
+  usually invisible \<open>Trueprop\<close>-coercions whenever necessary. 
   Consider for example the pairs
 
 @{ML_response [display,gray] "(@{term \"P x\"}, @{prop \"P x\"})" 
@@ -197,24 +197,24 @@
  Const (\"Pure.imp\", \<dots>) $ \<dots> $ \<dots>)"}
 
   where it is not (since it is already constructed by a meta-implication). 
-  The purpose of the @{text "Trueprop"}-coercion is to embed formulae of
+  The purpose of the \<open>Trueprop\<close>-coercion is to embed formulae of
   an object logic, for example HOL, into the meta-logic of Isabelle. The coercion
   is needed whenever a term is constructed that will be proved as a theorem. 
 
   As already seen above, types can be constructed using the antiquotation 
-  @{text "@{typ \<dots>}"}. For example:
+  \<open>@{typ \<dots>}\<close>. For example:
 
   @{ML_response_fake [display,gray] "@{typ \"bool \<Rightarrow> nat\"}" "bool \<Rightarrow> nat"}
 
   The corresponding datatype is
-*}
+\<close>
   
-ML_val %grayML{*datatype typ =
+ML_val %grayML\<open>datatype typ =
   Type  of string * typ list 
 | TFree of string * sort 
-| TVar  of indexname * sort *}
-
-text {*
+| TVar  of indexname * sort\<close>
+
+text \<open>
   Like with terms, there is the distinction between free type
   variables (term-constructor @{ML "TFree"}) and schematic
   type variables (term-constructor @{ML "TVar"} and printed with
@@ -222,19 +222,19 @@
   like @{typ "int"} or @{typ bool}, are types with an empty list
   of argument types. However, it needs a bit of effort to show an
   example, because Isabelle always pretty prints types (unlike terms).
-  Using just the antiquotation @{text "@{typ \"bool\"}"} we only see
+  Using just the antiquotation \<open>@{typ "bool"}\<close> we only see
 
   @{ML_response [display, gray]
   "@{typ \"bool\"}"
   "bool"}
-  which is the pretty printed version of @{text "bool"}. However, in PolyML
-  (version @{text "\<ge>"}5.3) it is easy to install your own pretty printer. With the
+  which is the pretty printed version of \<open>bool\<close>. However, in PolyML
+  (version \<open>\<ge>\<close>5.3) it is easy to install your own pretty printer. With the
   function below we mimic the behaviour of the usual pretty printer for
   datatypes (it uses pretty-printing functions which will be explained in more
   detail in Section~\ref{sec:pretty}).
-*}
-
-ML %grayML{*local
+\<close>
+
+ML %grayML\<open>local
   fun pp_pair (x, y) = Pretty.list "(" ")" [x, y]
   fun pp_list xs = Pretty.list "[" "]" xs
   fun pp_str s   = Pretty.str s
@@ -249,18 +249,18 @@
       pp_constr "TFree" (pp_pair (pp_qstr a, pp_sort S))
   | raw_pp_typ (Type (a, tys)) = 
       pp_constr "Type" (pp_pair (pp_qstr a, pp_list (map raw_pp_typ tys)))
-end*}
-
-text {*
+end\<close>
+
+text \<open>
   We can install this pretty printer with the function 
   @{ML_ind ML_system_pp} as follows.
-*}
-
-ML %grayML{*ML_system_pp
-  (fn _ => fn _ => Pretty.to_polyml o raw_pp_typ)*}
+\<close>
+
+ML %grayML\<open>ML_system_pp
+  (fn _ => fn _ => Pretty.to_polyml o raw_pp_typ)\<close>
 
 ML \<open>@{typ "bool"}\<close>
-text {*
+text \<open>
   Now the type bool is printed out in full detail.
 
   @{ML_response [display,gray]
@@ -273,10 +273,10 @@
   "@{typ \"'a list\"}"
   "Type (\"List.list\", [TFree (\"'a\", [\"HOL.type\"])])"}
 
-  we can see the full name of the type is actually @{text "List.list"}, indicating
-  that it is defined in the theory @{text "List"}. However, one has to be 
+  we can see the full name of the type is actually \<open>List.list\<close>, indicating
+  that it is defined in the theory \<open>List\<close>. However, one has to be 
   careful with names of types, because even if
-  @{text "fun"} is defined in the theory @{text "HOL"}, it is  
+  \<open>fun\<close> is defined in the theory \<open>HOL\<close>, it is  
   still represented by its simple name.
 
    @{ML_response [display,gray]
@@ -285,12 +285,12 @@
 
   We can restore the usual behaviour of Isabelle's pretty printer
   with the code
-*}
-
-ML %grayML{*ML_system_pp
-  (fn depth => fn _ => ML_Pretty.to_polyml o Pretty.to_ML depth o Proof_Display.pp_typ Theory.get_pure)*}
-
-text {*
+\<close>
+
+ML %grayML\<open>ML_system_pp
+  (fn depth => fn _ => ML_Pretty.to_polyml o Pretty.to_ML depth o Proof_Display.pp_typ Theory.get_pure)\<close>
+
+text \<open>
   After that the types for booleans, lists and so on are printed out again 
   the standard Isabelle way.
 
@@ -305,36 +305,36 @@
   definition and many useful operations are implemented 
   in @{ML_file "Pure/type.ML"}.
   \end{readmore}
-*}
-
-section {* Constructing Terms and Types Manually\label{sec:terms_types_manually} *} 
-
-text {*
+\<close>
+
+section \<open>Constructing Terms and Types Manually\label{sec:terms_types_manually}\<close> 
+
+text \<open>
   While antiquotations are very convenient for constructing terms, they can
   only construct fixed terms (remember they are ``linked'' at compile-time).
   However, you often need to construct terms manually. For example, a
-  function that returns the implication @{text "\<And>(x::nat). P x \<Longrightarrow> Q x"} taking
+  function that returns the implication \<open>\<And>(x::nat). P x \<Longrightarrow> Q x\<close> taking
   @{term P} and @{term Q} as arguments can only be written as:
 
-*}
-
-ML %grayML{*fun make_imp P Q =
+\<close>
+
+ML %grayML\<open>fun make_imp P Q =
 let
   val x = Free ("x", @{typ nat})
 in 
   Logic.all x (Logic.mk_implies (P $ x, Q $ x))
-end *}
-
-text {*
+end\<close>
+
+text \<open>
   The reason is that you cannot pass the arguments @{term P} and @{term Q} 
   into an antiquotation.\footnote{At least not at the moment.} For example 
   the following does \emph{not} work.
-*}
-
-ML %grayML{*fun make_wrong_imp P Q = @{prop "\<And>(x::nat). P x \<Longrightarrow> Q x"} *}
-
-text {*
-  To see this, apply @{text "@{term S}"} and @{text "@{term T}"} 
+\<close>
+
+ML %grayML\<open>fun make_wrong_imp P Q = @{prop "\<And>(x::nat). P x \<Longrightarrow> Q x"}\<close>
+
+text \<open>
+  To see this, apply \<open>@{term S}\<close> and \<open>@{term T}\<close> 
   to both functions. With @{ML make_imp} you obtain the intended term involving 
   the given arguments
 
@@ -344,7 +344,7 @@
     Const \<dots> $ (Free (\"S\",\<dots>) $ \<dots>) $ (Free (\"T\",\<dots>) $ \<dots>))"}
 
   whereas with @{ML make_wrong_imp} you obtain a term involving the @{term "P"} 
-  and @{text "Q"} from the antiquotation.
+  and \<open>Q\<close> from the antiquotation.
 
   @{ML_response [display,gray] "make_wrong_imp @{term S} @{term T}" 
 "Const \<dots> $ 
@@ -383,7 +383,7 @@
   In this example, @{ML lambda} produces a de Bruijn index (i.e.\ @{ML "Bound 0"}), 
   and an abstraction, where it also records the type of the abstracted
   variable and for printing purposes also its name.  Note that because of the
-  typing annotation on @{text "P"}, the variable @{text "x"} in @{text "P x"}
+  typing annotation on \<open>P\<close>, the variable \<open>x\<close> in \<open>P x\<close>
   is of the same type as the abstracted variable. If it is of different type,
   as in
 
@@ -396,7 +396,7 @@
 end"
   "Abs (\"x\", \"int\", Free (\"P\", \"nat \<Rightarrow> bool\") $ Free (\"x\", \"nat\"))"}
 
-  then the variable @{text "Free (\"x\", \"nat\")"} is \emph{not} abstracted. 
+  then the variable \<open>Free ("x", "nat")\<close> is \emph{not} abstracted. 
   This is a fundamental principle
   of Church-style typing, where variables with the same name still differ, if they 
   have different type.
@@ -431,18 +431,18 @@
   Similarly the function @{ML_ind subst_bounds in Term}, replaces lose bound 
   variables with terms. To see how this function works, let us implement a
   function that strips off the outermost forall quantifiers in a term.
-*}
-
-ML %grayML{*fun strip_alls t =
+\<close>
+
+ML %grayML\<open>fun strip_alls t =
 let 
   fun aux (x, T, t) = strip_alls t |>> cons (Free (x, T))
 in
   case t of
     Const (@{const_name All}, _) $ Abs body => aux body
   | _ => ([], t)
-end*}
-
-text {*
+end\<close>
+
+text \<open>
   The function returns a pair consisting of the stripped off variables and
   the body of the universal quantification. For example
 
@@ -454,14 +454,14 @@
   Note that we produced in the body two dangling de Bruijn indices. 
   Later on we will also use the inverse function that
   builds the quantification from a body and a list of (free) variables.
-*}
+\<close>
   
-ML %grayML{*fun build_alls ([], t) = t
+ML %grayML\<open>fun build_alls ([], t) = t
   | build_alls (Free (x, T) :: vs, t) = 
       Const (@{const_name "All"}, (T --> @{typ bool}) --> @{typ bool}) 
-        $ Abs (x, T, build_alls (vs, t))*}
-
-text {*
+        $ Abs (x, T, build_alls (vs, t))\<close>
+
+text \<open>
   As said above, after calling @{ML strip_alls}, you obtain a term with loose
   bound variables. With the function @{ML subst_bounds}, you can replace these
   loose @{ML_ind Bound in Term}s with the stripped off variables.
@@ -552,35 +552,35 @@
   When constructing terms manually, there are a few subtle issues with
   constants. They usually crop up when pattern matching terms or types, or
   when constructing them. While it is perfectly ok to write the function
-  @{text is_true} as follows
-*}
-
-ML %grayML{*fun is_true @{term True} = true
-  | is_true _ = false*}
-
-text {*
-  this does not work for picking out @{text "\<forall>"}-quantified terms. Because
+  \<open>is_true\<close> as follows
+\<close>
+
+ML %grayML\<open>fun is_true @{term True} = true
+  | is_true _ = false\<close>
+
+text \<open>
+  this does not work for picking out \<open>\<forall>\<close>-quantified terms. Because
   the function 
-*}
-
-ML %grayML{*fun is_all (@{term All} $ _) = true
-  | is_all _ = false*}
-
-text {* 
+\<close>
+
+ML %grayML\<open>fun is_all (@{term All} $ _) = true
+  | is_all _ = false\<close>
+
+text \<open>
   will not correctly match the formula @{prop[source] "\<forall>x::nat. P x"}: 
 
   @{ML_response [display,gray] "is_all @{term \"\<forall>x::nat. P x\"}" "false"}
 
-  The problem is that the @{text "@term"}-antiquotation in the pattern 
+  The problem is that the \<open>@term\<close>-antiquotation in the pattern 
   fixes the type of the constant @{term "All"} to be @{typ "('a \<Rightarrow> bool) \<Rightarrow> bool"} for 
   an arbitrary, but fixed type @{typ "'a"}. A properly working alternative 
   for this function is
-*}
-
-ML %grayML{*fun is_all (Const ("HOL.All", _) $ _) = true
-  | is_all _ = false*}
-
-text {* 
+\<close>
+
+ML %grayML\<open>fun is_all (Const ("HOL.All", _) $ _) = true
+  | is_all _ = false\<close>
+
+text \<open>
   because now
 
   @{ML_response [display,gray] "is_all @{term \"\<forall>x::nat. P x\"}" "true"}
@@ -589,13 +589,13 @@
   second any term).
 
   However there is still a problem: consider the similar function that
-  attempts to pick out @{text "Nil"}-terms:
-*}
-
-ML %grayML{*fun is_nil (Const ("Nil", _)) = true
-  | is_nil _ = false *}
-
-text {* 
+  attempts to pick out \<open>Nil\<close>-terms:
+\<close>
+
+ML %grayML\<open>fun is_nil (Const ("Nil", _)) = true
+  | is_nil _ = false\<close>
+
+text \<open>
   Unfortunately, also this function does \emph{not} work as expected, since
 
   @{ML_response [display,gray] "is_nil @{term \"Nil\"}" "false"}
@@ -607,9 +607,9 @@
 
   @{ML_response [display,gray] "@{term \"Nil\"}" "Const (\"List.list.Nil\", \<dots>)"}
 
-  the name of the constant @{text "Nil"} depends on the theory in which the
-  term constructor is defined (@{text "List"}) and also in which datatype
-  (@{text "list"}). Even worse, some constants have a name involving
+  the name of the constant \<open>Nil\<close> depends on the theory in which the
+  term constructor is defined (\<open>List\<close>) and also in which datatype
+  (\<open>list\<close>). Even worse, some constants have a name involving
   type-classes. Consider for example the constants for @{term "zero"} and
   \mbox{@{term "times"}}:
 
@@ -619,21 +619,21 @@
 
   While you could use the complete name, for example 
   @{ML "Const (\"List.list.Nil\", some_type)" for some_type}, for referring to or
-  matching against @{text "Nil"}, this would make the code rather brittle. 
+  matching against \<open>Nil\<close>, this would make the code rather brittle. 
   The reason is that the theory and the name of the datatype can easily change. 
   To make the code more robust, it is better to use the antiquotation 
-  @{text "@{const_name \<dots>}"}. With this antiquotation you can harness the 
+  \<open>@{const_name \<dots>}\<close>. With this antiquotation you can harness the 
   variable parts of the constant's name. Therefore a function for 
   matching against constants that have a polymorphic type should 
   be written as follows.
-*}
-
-ML %grayML{*fun is_nil_or_all (Const (@{const_name "Nil"}, _)) = true
+\<close>
+
+ML %grayML\<open>fun is_nil_or_all (Const (@{const_name "Nil"}, _)) = true
   | is_nil_or_all (Const (@{const_name "All"}, _) $ _) = true
-  | is_nil_or_all _ = false *}
-
-text {*
-  The antiquotation for properly referencing type constants is @{text "@{type_name \<dots>}"}.
+  | is_nil_or_all _ = false\<close>
+
+text \<open>
+  The antiquotation for properly referencing type constants is \<open>@{type_name \<dots>}\<close>.
   For example
 
   @{ML_response [display,gray]
@@ -644,34 +644,34 @@
   when defining constants. For example the function returning a function 
   type is as follows:
 
-*} 
-
-ML %grayML{*fun make_fun_type ty1 ty2 = Type ("fun", [ty1, ty2]) *}
-
-text {* This can be equally written with the combinator @{ML_ind "-->" in Term} as: *}
-
-ML %grayML{*fun make_fun_type ty1 ty2 = ty1 --> ty2 *}
-
-text {*
+\<close> 
+
+ML %grayML\<open>fun make_fun_type ty1 ty2 = Type ("fun", [ty1, ty2])\<close>
+
+text \<open>This can be equally written with the combinator @{ML_ind "-->" in Term} as:\<close>
+
+ML %grayML\<open>fun make_fun_type ty1 ty2 = ty1 --> ty2\<close>
+
+text \<open>
   If you want to construct a function type with more than one argument
   type, then you can use @{ML_ind "--->" in Term}.
-*}
-
-ML %grayML{*fun make_fun_types tys ty = tys ---> ty *}
-
-text {*
+\<close>
+
+ML %grayML\<open>fun make_fun_types tys ty = tys ---> ty\<close>
+
+text \<open>
   A handy function for manipulating terms is @{ML_ind map_types in Term}: it takes a 
   function and applies it to every type in a term. You can, for example,
   change every @{typ nat} in a term into an @{typ int} using the function:
-*}
-
-ML %grayML{*fun nat_to_int ty =
+\<close>
+
+ML %grayML\<open>fun nat_to_int ty =
   (case ty of
      @{typ nat} => @{typ int}
    | Type (s, tys) => Type (s, map nat_to_int tys)
-   | _ => ty)*}
-
-text {*
+   | _ => ty)\<close>
+
+text \<open>
   Here is an example:
 
 @{ML_response_fake [display,gray] 
@@ -697,13 +697,13 @@
 
   The reason for this definition is that @{ML add_tfrees in Term} can
   be easily folded over a list of terms. Similarly for all functions
-  named @{text "add_*"} in @{ML_file "Pure/term.ML"}.
+  named \<open>add_*\<close> in @{ML_file "Pure/term.ML"}.
 
   \begin{exercise}\label{fun:revsum}
-  Write a function @{text "rev_sum : term -> term"} that takes a
-  term of the form @{text "t\<^sub>1 + t\<^sub>2 + \<dots> + t\<^sub>n"} (whereby @{text "n"} might be one)
-  and returns the reversed sum @{text "t\<^sub>n + \<dots> + t\<^sub>2 + t\<^sub>1"}. Assume
-  the @{text "t\<^sub>i"} can be arbitrary expressions and also note that @{text "+"} 
+  Write a function \<open>rev_sum : term -> term\<close> that takes a
+  term of the form \<open>t\<^sub>1 + t\<^sub>2 + \<dots> + t\<^sub>n\<close> (whereby \<open>n\<close> might be one)
+  and returns the reversed sum \<open>t\<^sub>n + \<dots> + t\<^sub>2 + t\<^sub>1\<close>. Assume
+  the \<open>t\<^sub>i\<close> can be arbitrary expressions and also note that \<open>+\<close> 
   associates to the left. Try your function on some examples. 
   \end{exercise}
 
@@ -722,8 +722,8 @@
   \end{exercise}
 
   \begin{exercise}\label{fun:makelist}
-  Write a function that takes an integer @{text i} and
-  produces an Isabelle integer list from @{text 1} upto @{text i}, 
+  Write a function that takes an integer \<open>i\<close> and
+  produces an Isabelle integer list from \<open>1\<close> upto \<open>i\<close>, 
   and then builds the reverse of this list using @{const rev}. 
   The relevant helper functions are @{ML upto}, 
   @{ML HOLogic.mk_number} and @{ML HOLogic.mk_list}.
@@ -756,11 +756,11 @@
   for constructing the terms for the logical connectives.\footnote{Thanks to Roy
   Dyckhoff for suggesting this exercise and working out the details.} 
   \end{exercise}
-*}
-
-section {* Unification and Matching\label{sec:univ} *}
-
-text {* 
+\<close>
+
+section \<open>Unification and Matching\label{sec:univ}\<close>
+
+text \<open>
   As seen earlier, Isabelle's terms and types may contain schematic term variables
   (term-constructor @{ML Var}) and schematic type variables (term-constructor
   @{ML TVar}). These variables stand for unknown entities, which can be made
@@ -769,7 +769,7 @@
   relatively straightforward, in case of terms the algorithms are
   substantially more complicated, because terms need higher-order versions of
   the unification and matching algorithms. Below we shall use the
-  antiquotations @{text "@{typ_pat \<dots>}"} and @{text "@{term_pat \<dots>}"} from
+  antiquotations \<open>@{typ_pat \<dots>}\<close> and \<open>@{term_pat \<dots>}\<close> from
   Section~\ref{sec:antiquote} in order to construct examples involving
   schematic variables.
 
@@ -777,24 +777,24 @@
   types.  Both return type environments (ML-type @{ML_type "Type.tyenv"})
   which map schematic type variables to types and sorts. Below we use the
   function @{ML_ind typ_unify in Sign} from the structure @{ML_struct Sign}
-  for unifying the types @{text "?'a * ?'b"} and @{text "?'b list *
-  nat"}. This will produce the mapping, or type environment, @{text "[?'a :=
-  ?'b list, ?'b := nat]"}.
-*}
-
-ML %linenosgray{*val (tyenv_unif, _) = let
+  for unifying the types \<open>?'a * ?'b\<close> and \<open>?'b list *
+  nat\<close>. This will produce the mapping, or type environment, \<open>[?'a :=
+  ?'b list, ?'b := nat]\<close>.
+\<close>
+
+ML %linenosgray\<open>val (tyenv_unif, _) = let
   val ty1 = @{typ_pat "?'a * ?'b"}
   val ty2 = @{typ_pat "?'b list * nat"}
 in
   Sign.typ_unify @{theory} (ty1, ty2) (Vartab.empty, 0) 
-end*}
-
-text {* 
+end\<close>
+
+text \<open>
   The environment @{ML_ind "Vartab.empty"} in line 5 stands for the empty type
   environment, which is needed for starting the unification without any
-  (pre)instantiations. The @{text 0} is an integer index that will be explained
+  (pre)instantiations. The \<open>0\<close> is an integer index that will be explained
   below. In case of failure, @{ML typ_unify in Sign} will raise the exception
-  @{text TUNIFY}.  We can print out the resulting type environment bound to 
+  \<open>TUNIFY\<close>.  We can print out the resulting type environment bound to 
   @{ML tyenv_unif} with the built-in function @{ML_ind dest in Vartab} from the
   structure @{ML_struct Vartab}.
 
@@ -802,13 +802,13 @@
   "Vartab.dest tyenv_unif"
   "[((\"'a\", 0), ([\"HOL.type\"], \"?'b List.list\")), 
  ((\"'b\", 0), ([\"HOL.type\"], \"nat\"))]"} 
-*}
-
-text_raw {*
+\<close>
+
+text_raw \<open>
   \begin{figure}[t]
   \begin{minipage}{\textwidth}
-  \begin{isabelle}*}
-ML %grayML{*fun pretty_helper aux env =
+  \begin{isabelle}\<close>
+ML %grayML\<open>fun pretty_helper aux env =
   env |> Vartab.dest  
       |> map aux
       |> map (fn (s1, s2) => Pretty.block [s1, Pretty.str " := ", s2]) 
@@ -821,19 +821,19 @@
   val print = apply2 (pretty_typ ctxt)
 in 
   pretty_helper (print o get_typs) tyenv
-end*}
-text_raw {*
+end\<close>
+text_raw \<open>
   \end{isabelle}
   \end{minipage}
   \caption{A pretty printing function for type environments, which are 
   produced by unification and matching.\label{fig:prettyenv}}
   \end{figure}
-*}
-
-text {*
+\<close>
+
+text \<open>
   The first components in this list stand for the schematic type variables and
   the second are the associated sorts and types. In this example the sort is
-  the default sort @{text "HOL.type"}. Instead of @{ML "Vartab.dest"}, we will
+  the default sort \<open>HOL.type\<close>. Instead of @{ML "Vartab.dest"}, we will
   use in what follows our own pretty-printing function from
   Figure~\ref{fig:prettyenv} for @{ML_type "Type.tyenv"}s. For the type
   environment in the example this function prints out the more legible:
@@ -846,38 +846,38 @@
   The way the unification function @{ML typ_unify in Sign} is implemented 
   using an initial type environment and initial index makes it easy to
   unify more than two terms. For example 
-*}
-
-ML %linenosgray{*val (tyenvs, _) = let
+\<close>
+
+ML %linenosgray\<open>val (tyenvs, _) = let
   val tys1 = (@{typ_pat "?'a"}, @{typ_pat "?'b list"})
   val tys2 = (@{typ_pat "?'b"}, @{typ_pat "nat"})
 in
   fold (Sign.typ_unify @{theory}) [tys1, tys2] (Vartab.empty, 0) 
-end*}
-
-text {*
-  The index @{text 0} in Line 5 is the maximal index of the schematic type
-  variables occurring in @{text tys1} and @{text tys2}. This index will be
+end\<close>
+
+text \<open>
+  The index \<open>0\<close> in Line 5 is the maximal index of the schematic type
+  variables occurring in \<open>tys1\<close> and \<open>tys2\<close>. This index will be
   increased whenever a new schematic type variable is introduced during
   unification.  This is for example the case when two schematic type variables
   have different, incomparable sorts. Then a new schematic type variable is
   introduced with the combined sorts. To show this let us assume two sorts,
-  say @{text "s1"} and @{text "s2"}, which we attach to the schematic type
-  variables @{text "?'a"} and @{text "?'b"}. Since we do not make any
+  say \<open>s1\<close> and \<open>s2\<close>, which we attach to the schematic type
+  variables \<open>?'a\<close> and \<open>?'b\<close>. Since we do not make any
   assumption about the sorts, they are incomparable.
-*}
+\<close>
 
 class s1
 class s2 
 
-ML %grayML{*val (tyenv, index) = let
+ML %grayML\<open>val (tyenv, index) = let
   val ty1 = @{typ_pat "?'a::s1"}
   val ty2 = @{typ_pat "?'b::s2"}
 in
   Sign.typ_unify @{theory} (ty1, ty2) (Vartab.empty, 0) 
-end*}
-
-text {*
+end\<close>
+
+text \<open>
   To print out the result type environment we switch on the printing 
   of sort information by setting @{ML_ind show_sorts in Syntax} to 
   true. This allows us to inspect the typing environment.
@@ -886,17 +886,17 @@
   "pretty_tyenv @{context} tyenv"
   "[?'a::s1 := ?'a1::{s1, s2}, ?'b::s2 := ?'a1::{s1, s2}]"}
 
-  As can be seen, the type variables @{text "?'a"} and @{text "?'b"} are instantiated
-  with a new type variable @{text "?'a1"} with sort @{text "{s1, s2}"}. Since a new
-  type variable has been introduced the @{ML index}, originally being @{text 0}, 
-  has been increased to @{text 1}.
+  As can be seen, the type variables \<open>?'a\<close> and \<open>?'b\<close> are instantiated
+  with a new type variable \<open>?'a1\<close> with sort \<open>{s1, s2}\<close>. Since a new
+  type variable has been introduced the @{ML index}, originally being \<open>0\<close>, 
+  has been increased to \<open>1\<close>.
 
   @{ML_response [display,gray]
   "index"
   "1"}
 
-  Let us now return to the unification problem @{text "?'a * ?'b"} and 
-  @{text "?'b list * nat"} from the beginning of this section, and the 
+  Let us now return to the unification problem \<open>?'a * ?'b\<close> and 
+  \<open>?'b list * nat\<close> from the beginning of this section, and the 
   calculated type environment @{ML tyenv_unif}:
 
   @{ML_response_fake [display, gray]
@@ -904,13 +904,12 @@
   "[?'a := ?'b list, ?'b := nat]"}
 
   Observe that the type environment which the function @{ML typ_unify in
-  Sign} returns is \emph{not} an instantiation in fully solved form: while @{text
-  "?'b"} is instantiated to @{typ nat}, this is not propagated to the
-  instantiation for @{text "?'a"}.  In unification theory, this is often
+  Sign} returns is \emph{not} an instantiation in fully solved form: while \<open>?'b\<close> is instantiated to @{typ nat}, this is not propagated to the
+  instantiation for \<open>?'a\<close>.  In unification theory, this is often
   called an instantiation in \emph{triangular form}. These triangular 
   instantiations, or triangular type environments, are used because of 
-  performance reasons. To apply such a type environment to a type, say @{text "?'a *
-  ?'b"}, you should use the function @{ML_ind norm_type in Envir}:
+  performance reasons. To apply such a type environment to a type, say \<open>?'a *
+  ?'b\<close>, you should use the function @{ML_ind norm_type in Envir}:
 
   @{ML_response_fake [display, gray]
   "Envir.norm_type tyenv_unif @{typ_pat \"?'a * ?'b\"}"
@@ -918,18 +917,18 @@
 
   Matching of types can be done with the function @{ML_ind typ_match in Sign}
   also from the structure @{ML_struct Sign}. This function returns a @{ML_type
-  Type.tyenv} as well, but might raise the exception @{text TYPE_MATCH} in case
+  Type.tyenv} as well, but might raise the exception \<open>TYPE_MATCH\<close> in case
   of failure. For example
-*}
-
-ML %grayML{*val tyenv_match = let
+\<close>
+
+ML %grayML\<open>val tyenv_match = let
   val pat = @{typ_pat "?'a * ?'b"}
   and ty  = @{typ_pat "bool list * nat"}
 in
   Sign.typ_match @{theory} (pat, ty) Vartab.empty 
-end*}
-
-text {*
+end\<close>
+
+text \<open>
   Printing out the calculated matcher gives
 
   @{ML_response_fake [display,gray]
@@ -948,18 +947,18 @@
   @{ML subst_type in Envir} for matchers and @{ML norm_type in Envir} 
   for unifiers. To show the difference, let us calculate the 
   following matcher:
-*}
-
-ML %grayML{*val tyenv_match' = let
+\<close>
+
+ML %grayML\<open>val tyenv_match' = let
   val pat = @{typ_pat "?'a * ?'b"}
   and ty  = @{typ_pat "?'b list * nat"}
 in
   Sign.typ_match @{theory} (pat, ty) Vartab.empty 
-end*}
-
-text {*
+end\<close>
+
+text \<open>
   Now @{ML tyenv_unif} is equal to @{ML tyenv_match'}. If we apply 
-  @{ML norm_type in Envir} to the type @{text "?'a * ?'b"} we obtain
+  @{ML norm_type in Envir} to the type \<open>?'a * ?'b\<close> we obtain
 
   @{ML_response_fake [display, gray]
   "Envir.norm_type tyenv_match' @{typ_pat \"?'a * ?'b\"}"
@@ -983,43 +982,43 @@
   which apply a type environment to a type. Type environments are lookup 
   tables which are implemented in @{ML_file "Pure/term_ord.ML"}.
   \end{readmore}
-*}
-
-text {*
+\<close>
+
+text \<open>
   Unification and matching of terms is substantially more complicated than the
   type-case. The reason is that terms have abstractions and, in this context,  
   unification or matching modulo plain equality is often not meaningful. 
   Nevertheless, Isabelle implements the function @{ML_ind
   first_order_match in Pattern} for terms.  This matching function returns a
   type environment and a term environment.  To pretty print the latter we use
-  the function @{text "pretty_env"}:
-*}
-
-ML %grayML{*fun pretty_env ctxt env =
+  the function \<open>pretty_env\<close>:
+\<close>
+
+ML %grayML\<open>fun pretty_env ctxt env =
 let
   fun get_trms (v, (T, t)) = (Var (v, T), t) 
   val print = apply2 (pretty_term ctxt)
 in
   pretty_helper (print o get_trms) env 
-end*}
-
-text {*
-  As can be seen from the @{text "get_trms"}-function, a term environment associates 
+end\<close>
+
+text \<open>
+  As can be seen from the \<open>get_trms\<close>-function, a term environment associates 
   a schematic term variable with a type and a term.  An example of a first-order 
   matching problem is the term @{term "P (\<lambda>a b. Q b a)"} and the pattern 
-  @{text "?X ?Y"}.
-*}
-
-ML %grayML{*val (_, fo_env) = let
+  \<open>?X ?Y\<close>.
+\<close>
+
+ML %grayML\<open>val (_, fo_env) = let
   val fo_pat = @{term_pat "(?X::(nat\<Rightarrow>nat\<Rightarrow>nat)\<Rightarrow>bool) ?Y"}
   val trm_a = @{term "P::(nat\<Rightarrow>nat\<Rightarrow>nat)\<Rightarrow>bool"} 
   val trm_b = @{term "\<lambda>a b. (Q::nat\<Rightarrow>nat\<Rightarrow>nat) b a"}
   val init = (Vartab.empty, Vartab.empty) 
 in
   Pattern.first_order_match @{theory} (fo_pat, trm_a $ trm_b) init
-end *}
-
-text {*
+end\<close>
+
+text \<open>
   In this example we annotated types explicitly because then 
   the type environment is empty and can be ignored. The 
   resulting term environment is
@@ -1048,8 +1047,8 @@
   variables. It can also deal with abstractions and a limited form of
   alpha-equivalence, but this kind of matching should be used with care, since
   it is not clear whether the result is meaningful. A meaningful example is
-  matching @{text "\<lambda>x. P x"} against the pattern @{text "\<lambda>y. ?X y"}. In this
-  case, first-order matching produces @{text "[?X := P]"}.
+  matching \<open>\<lambda>x. P x\<close> against the pattern \<open>\<lambda>y. ?X y\<close>. In this
+  case, first-order matching produces \<open>[?X := P]\<close>.
 
   @{ML_response_fake [display, gray]
   "let
@@ -1062,9 +1061,9 @@
   |> pretty_env @{context} 
 end"
   "[?X := P]"}
-*}
-
-text {*
+\<close>
+
+text \<open>
   Unification of abstractions is more thoroughly studied in the context of
   higher-order pattern unification and higher-order pattern matching.  A
   \emph{\index*{pattern}} is a well-formed term in which the arguments to
@@ -1114,42 +1113,41 @@
   "[?X := \<lambda>y x. x, ?Y := \<lambda>x. x]"}
 
   The function @{ML_ind "Envir.empty"} generates a record with a specified
-  max-index for the schematic variables (in the example the index is @{text
-  0}) and empty type and term environments. The function @{ML_ind
+  max-index for the schematic variables (in the example the index is \<open>0\<close>) and empty type and term environments. The function @{ML_ind
   "Envir.term_env"} pulls out the term environment from the result record. The
   corresponding function for type environment is @{ML_ind
   "Envir.type_env"}. An assumption of this function is that the terms to be
   unified have already the same type. In case of failure, the exceptions that
-  are raised are either @{text Pattern}, @{text MATCH} or @{text Unif}.
+  are raised are either \<open>Pattern\<close>, \<open>MATCH\<close> or \<open>Unif\<close>.
 
   As mentioned before, unrestricted higher-order unification, respectively
   unrestricted higher-order matching, is in general undecidable and might also
   not possess a single most general solution. Therefore Isabelle implements the
   unification function @{ML_ind unifiers in Unify} so that it returns a lazy
   list of potentially infinite unifiers.  An example is as follows
-*}
-
-ML %grayML{*val uni_seq =
+\<close>
+
+ML %grayML\<open>val uni_seq =
 let 
   val trm1 = @{term_pat "?X ?Y"}
   val trm2 = @{term "f a"}
   val init = Envir.empty 0
 in
   Unify.unifiers (Context.Proof @{context}, init, [(trm1, trm2)])
-end *}
-
-text {*
+end\<close>
+
+text \<open>
   The unifiers can be extracted from the lazy sequence using the 
   function @{ML_ind "Seq.pull"}. In the example we obtain three 
-  unifiers @{text "un1\<dots>un3"}.
-*}
-
-ML %grayML{*val SOME ((un1, _), next1) = Seq.pull uni_seq;
+  unifiers \<open>un1\<dots>un3\<close>.
+\<close>
+
+ML %grayML\<open>val SOME ((un1, _), next1) = Seq.pull uni_seq;
 val SOME ((un2, _), next2) = Seq.pull next1;
 val SOME ((un3, _), next3) = Seq.pull next2;
-val NONE = Seq.pull next3 *}
-
-text {*
+val NONE = Seq.pull next3\<close>
+
+text \<open>
   \footnote{\bf FIXME: what is the list of term pairs in the unifier: flex-flex pairs?}
 
   We can print them out as follows.
@@ -1207,20 +1205,20 @@
 
   \begin{isabelle}
   \isacommand{thm}~@{thm [source] spec}\\
-  @{text "> "}~@{thm spec}
+  \<open>> \<close>~@{thm spec}
   \end{isabelle}
 
   as an introduction rule. Applying it directly can lead to unexpected
   behaviour since the unification has more than one solution. One way round
-  this problem is to instantiate the schematic variables @{text "?P"} and
-  @{text "?x"}.  Instantiation function for theorems is 
+  this problem is to instantiate the schematic variables \<open>?P\<close> and
+  \<open>?x\<close>.  Instantiation function for theorems is 
   @{ML_ind instantiate_normalize in Drule} from the structure 
   @{ML_struct Drule}. One problem, however, is
   that this function expects the instantiations as lists of @{ML_type "((indexname * sort) * ctyp)"}
   respective @{ML_type "(indexname * typ) * cterm"}:
 
   \begin{isabelle}
-  @{ML instantiate_normalize in Drule}@{text ":"}
+  @{ML instantiate_normalize in Drule}\<open>:\<close>
   @{ML_type "((indexname * sort) * ctyp) list * ((indexname * typ) * cterm) list -> thm -> thm"}
   \end{isabelle}
 
@@ -1230,23 +1228,23 @@
   from an environment the corresponding variable mappings for schematic type 
   and term variables. These mappings can be turned into proper 
   @{ML_type ctyp}-pairs with the function
-*}
-
-ML %grayML{*fun prep_trm ctxt (x, (T, t)) = 
-  ((x, T), Thm.cterm_of ctxt t)*} 
-
-text {*
+\<close>
+
+ML %grayML\<open>fun prep_trm ctxt (x, (T, t)) = 
+  ((x, T), Thm.cterm_of ctxt t)\<close> 
+
+text \<open>
   and into proper @{ML_type cterm}-pairs with
-*}
-
-ML %grayML{*fun prep_ty ctxt (x, (S, ty)) = 
-  ((x, S), Thm.ctyp_of ctxt ty)*}
-
-text {*
+\<close>
+
+ML %grayML\<open>fun prep_ty ctxt (x, (S, ty)) = 
+  ((x, S), Thm.ctyp_of ctxt ty)\<close>
+
+text \<open>
   We can now calculate the instantiations from the matching function. 
-*}
-
-ML %linenosgray{*fun matcher_inst ctxt pat trm i = 
+\<close>
+
+ML %linenosgray\<open>fun matcher_inst ctxt pat trm i = 
 let
   val univ = Unify.matchers (Context.Proof ctxt) [(pat, trm)] 
   val env = nth (Seq.list_of univ) i
@@ -1254,13 +1252,13 @@
   val tyenv = Vartab.dest (Envir.type_env env)
 in
   (map (prep_ty ctxt) tyenv, map (prep_trm ctxt) tenv)
-end*}
+end\<close>
 
 ML \<open>Context.get_generic_context\<close>
-text {*
+text \<open>
   In Line 3 we obtain the higher-order matcher. We assume there is a finite
   number of them and select the one we are interested in via the parameter 
-  @{text i} in the next line. In Lines 5 and 6 we destruct the resulting 
+  \<open>i\<close> in the next line. In Lines 5 and 6 we destruct the resulting 
   environments using the function @{ML_ind dest in Vartab}. Finally, we need 
   to map the functions @{ML prep_trm} and @{ML prep_ty} over the respective 
   environments (Line 8). As a simple example we instantiate the
@@ -1278,7 +1276,7 @@
 end"
   "\<forall>x. Q x \<Longrightarrow> Q True"}
 
-  Note that we had to insert a @{text "Trueprop"}-coercion in Line 3 since the 
+  Note that we had to insert a \<open>Trueprop\<close>-coercion in Line 3 since the 
   conclusion of @{thm [source] spec} contains one.
  
   \begin{readmore}
@@ -1288,11 +1286,11 @@
   in @{ML_file "Pure/unify.ML"}. It uses lazy sequences which are implemented
   in @{ML_file "Pure/General/seq.ML"}.
   \end{readmore}
-*}
-
-section {* Sorts (TBD)\label{sec:sorts} *}
-
-text {*
+\<close>
+
+section \<open>Sorts (TBD)\label{sec:sorts}\<close>
+
+text \<open>
   Type classes are formal names in the type system which are linked to
   predicates of one type variable (via the axclass mechanism) and thereby
   express extra properties on types, to be propagated by the type system.
@@ -1320,14 +1318,14 @@
   Free and schematic type variables are always annotated with sorts, thereby restricting
   the domain of types they quantify over and corresponding to an implicit hypothesis
   about the type variable.
-*}
-
-
-ML {* Sign.classes_of @{theory} *}
-
-ML {* Sign.of_sort @{theory} *}
-
-text {*
+\<close>
+
+
+ML \<open>Sign.classes_of @{theory}\<close>
+
+ML \<open>Sign.of_sort @{theory}\<close>
+
+text \<open>
   \begin{readmore}
   Classes, sorts and arities are defined in @{ML_file "Pure/term.ML"}.
   
@@ -1344,12 +1342,12 @@
     functionality.
     It also provides the most needed functionality from individual underlying modules.
   \end{readmore}
-*}
-
-
-section {* Type-Checking\label{sec:typechecking} *}
-
-text {* 
+\<close>
+
+
+section \<open>Type-Checking\label{sec:typechecking}\<close>
+
+text \<open>
   Remember Isabelle follows the Church-style typing for terms, i.e.\ a term contains 
   enough typing information (constants, free variables and abstractions all have typing 
   information) so that it is always clear what the type of a term is. 
@@ -1400,8 +1398,8 @@
 "Const (\"HOL.plus_class.plus\", \"nat \<Rightarrow> nat \<Rightarrow> nat\") $
   Const (\"HOL.one_class.one\", \"nat\") $ Free (\"x\", \"nat\")"}
 
-  Instead of giving explicitly the type for the constant @{text "plus"} and the free 
-  variable @{text "x"}, type-inference fills in the missing information.
+  Instead of giving explicitly the type for the constant \<open>plus\<close> and the free 
+  variable \<open>x\<close>, type-inference fills in the missing information.
 
   \begin{readmore}
   See @{ML_file "Pure/Syntax/syntax.ML"} where more functions about reading,
@@ -1417,11 +1415,11 @@
   exercise given in Appendix \ref{ch:solutions} when they receive an 
   ill-typed term as input.
   \end{exercise}
-*}
-
-section {* Certified Terms and Certified Types *}
-
-text {*
+\<close>
+
+section \<open>Certified Terms and Certified Types\<close>
+
+text \<open>
   You can freely construct and manipulate @{ML_type "term"}s and @{ML_type
   typ}es, since they are just arbitrary unchecked trees. However, you
   eventually want to see if a term is well-formed, or type-checks, relative to
@@ -1502,11 +1500,11 @@
   the files @{ML_file "Pure/thm.ML"}, @{ML_file "Pure/more_thm.ML"} and
   @{ML_file "Pure/drule.ML"}.
   \end{readmore}
-*}
-
-section {* Theorems\label{sec:theorems} *}
-
-text {*
+\<close>
+
+section \<open>Theorems\label{sec:theorems}\<close>
+
+text \<open>
   Just like @{ML_type cterm}s, theorems are abstract objects of type @{ML_type thm} 
   that can only be built by going through interfaces. As a consequence, every proof 
   in Isabelle is correct by construction. This follows the tradition of the LCF-approach.
@@ -1514,18 +1512,18 @@
 
   To see theorems in ``action'', let us give a proof on the ML-level for the following 
   statement:
-*}
+\<close>
 
   lemma 
     assumes assm\<^sub>1: "\<And>(x::nat). P x \<Longrightarrow> Q x" 
     and     assm\<^sub>2: "P t"
     shows "Q t"(*<*)oops(*>*) 
 
-text {*
+text \<open>
   The corresponding ML-code is as follows:
-*}
-
-ML %linenosgray{*val my_thm = 
+\<close>
+
+ML %linenosgray\<open>val my_thm = 
 let
   val assm1 = @{cprop "\<And>(x::nat). P x \<Longrightarrow> Q x"}
   val assm2 = @{cprop "(P::nat \<Rightarrow> bool) t"}
@@ -1539,11 +1537,11 @@
   Qt 
   |> Thm.implies_intr assm2
   |> Thm.implies_intr assm1
-end*}
-
-text {*
-  Note that in Line 3 and 4 we use the antiquotation @{text "@{cprop \<dots>}"}, which
-  inserts necessary @{text "Trueprop"}s.
+end\<close>
+
+text \<open>
+  Note that in Line 3 and 4 we use the antiquotation \<open>@{cprop \<dots>}\<close>, which
+  inserts necessary \<open>Trueprop\<close>s.
 
   If we print out the value of @{ML my_thm} then we see only the 
   final statement of the theorem.
@@ -1556,10 +1554,10 @@
   proof.
 
   \[
-  \infer[(@{text "\<Longrightarrow>"}$-$intro)]{\vdash @{prop "(\<And>x. P x \<Longrightarrow> Q x) \<Longrightarrow> P t \<Longrightarrow> Q t"}}
-    {\infer[(@{text "\<Longrightarrow>"}$-$intro)]{@{prop "\<And>x. P x \<Longrightarrow> Q x"} \vdash @{prop "P t \<Longrightarrow> Q t"}}
-       {\infer[(@{text "\<Longrightarrow>"}$-$elim)]{@{prop "\<And>x. P x \<Longrightarrow> Q x"}, @{prop "P t"} \vdash @{prop "Q t"}}
-          {\infer[(@{text "\<And>"}$-$elim)]{@{prop "\<And>x. P x \<Longrightarrow> Q x"} \vdash @{prop "P t \<Longrightarrow> Q t"}}
+  \infer[(\<open>\<Longrightarrow>\<close>$-$intro)]{\vdash @{prop "(\<And>x. P x \<Longrightarrow> Q x) \<Longrightarrow> P t \<Longrightarrow> Q t"}}
+    {\infer[(\<open>\<Longrightarrow>\<close>$-$intro)]{@{prop "\<And>x. P x \<Longrightarrow> Q x"} \vdash @{prop "P t \<Longrightarrow> Q t"}}
+       {\infer[(\<open>\<Longrightarrow>\<close>$-$elim)]{@{prop "\<And>x. P x \<Longrightarrow> Q x"}, @{prop "P t"} \vdash @{prop "Q t"}}
+          {\infer[(\<open>\<And>\<close>$-$elim)]{@{prop "\<And>x. P x \<Longrightarrow> Q x"} \vdash @{prop "P t \<Longrightarrow> Q t"}}
                  {\infer[(assume)]{@{prop "\<And>x. P x \<Longrightarrow> Q x"} \vdash @{prop "\<And>x. P x \<Longrightarrow> Q x"}}{}}
                  &
            \infer[(assume)]{@{prop "P t"} \vdash @{prop "P t"}}{}
@@ -1575,22 +1573,22 @@
   @{ML_struct Local_Theory} (the Isabelle command
   \isacommand{local\_setup} will be explained in more detail in 
   Section~\ref{sec:local}).
-*}
+\<close>
 
 (*FIXME: add forward reference to Proof_Context.export *)
-ML %linenosgray{*val my_thm_vars =
+ML %linenosgray\<open>val my_thm_vars =
 let
   val ctxt0 = @{context}
   val (_, ctxt1) = Variable.add_fixes ["P", "Q", "t"] ctxt0
 in
   singleton (Proof_Context.export ctxt1 ctxt0) my_thm
-end*}
-
-local_setup %gray {*
-  Local_Theory.note ((@{binding "my_thm"}, []), [my_thm_vars]) #> snd *}
-
-
-text {*
+end\<close>
+
+local_setup %gray \<open>
+  Local_Theory.note ((@{binding "my_thm"}, []), [my_thm_vars]) #> snd\<close>
+
+
+text \<open>
   The third argument of @{ML note in Local_Theory} is the list of theorems we
   want to store under a name. We can store more than one under a single name. 
   The first argument of @{ML note in Local_Theory} is the name under
@@ -1598,13 +1596,13 @@
   list of theorem attributes, which we will explain in detail in
   Section~\ref{sec:attributes}. Below we just use one such attribute,
   @{ML_ind simp_add in Simplifier}, for adding the theorem to the simpset:
-*}
-
-local_setup %gray {*
+\<close>
+
+local_setup %gray \<open>
   Local_Theory.note ((@{binding "my_thm_simp"}, 
-       [Attrib.internal (K Simplifier.simp_add)]), [my_thm_vars]) #> snd *}
-
-text {*
+       [Attrib.internal (K Simplifier.simp_add)]), [my_thm_vars]) #> snd\<close>
+
+text \<open>
   Note that we have to use another name under which the theorem is stored,
   since Isabelle does not allow us to call  @{ML_ind note in Local_Theory} twice
   with the same name. The attribute needs to be wrapped inside the function @{ML_ind
@@ -1628,12 +1626,12 @@
 
     
   \begin{isabelle}
-  \isacommand{thm}~@{text "my_thm my_thm_simp"}\isanewline
-  @{text ">"}~@{prop "\<lbrakk>\<And>x. P x \<Longrightarrow> Q x; P t\<rbrakk> \<Longrightarrow> Q t"}\isanewline
-  @{text ">"}~@{prop "\<lbrakk>\<And>x. P x \<Longrightarrow> Q x; P t\<rbrakk> \<Longrightarrow> Q t"}
+  \isacommand{thm}~\<open>my_thm my_thm_simp\<close>\isanewline
+  \<open>>\<close>~@{prop "\<lbrakk>\<And>x. P x \<Longrightarrow> Q x; P t\<rbrakk> \<Longrightarrow> Q t"}\isanewline
+  \<open>>\<close>~@{prop "\<lbrakk>\<And>x. P x \<Longrightarrow> Q x; P t\<rbrakk> \<Longrightarrow> Q t"}
   \end{isabelle}
 
-  or with the @{text "@{thm \<dots>}"}-antiquotation on the ML-level. Otherwise the 
+  or with the \<open>@{thm \<dots>}\<close>-antiquotation on the ML-level. Otherwise the 
   user has no access to these theorems. 
 
   Recall that Isabelle does not let you call @{ML note in Local_Theory} twice
@@ -1644,78 +1642,78 @@
   dynamically expanding list of theorems (like a simpset). Therefore Isabelle 
   also implements a mechanism where a theorem name can refer to a custom theorem 
   list. For this you can use the function @{ML_ind add_thms_dynamic in Global_Theory}. 
-  To see how it works let us assume we defined our own theorem list @{text MyThmList}.
-*}
-
-ML %grayML{*structure MyThmList = Generic_Data
+  To see how it works let us assume we defined our own theorem list \<open>MyThmList\<close>.
+\<close>
+
+ML %grayML\<open>structure MyThmList = Generic_Data
   (type T = thm list
    val empty = []
    val extend = I
    val merge = merge Thm.eq_thm_prop)
 
-fun update thm = Context.theory_map (MyThmList.map (Thm.add_thm thm))*}
-
-text {*
+fun update thm = Context.theory_map (MyThmList.map (Thm.add_thm thm))\<close>
+
+text \<open>
   The function @{ML update} allows us to update the theorem list, for example
   by adding the theorem @{thm [source] TrueI}.
-*}
-
-setup %gray {* update @{thm TrueI} *}
+\<close>
+
+setup %gray \<open>update @{thm TrueI}\<close>
  
-text {*
+text \<open>
   We can now install the theorem list so that it is visible to the user and 
   can be refered to by a theorem name. For this need to call 
   @{ML_ind add_thms_dynamic in Global_Theory}
-*}
-
-setup %gray {* 
+\<close>
+
+setup %gray \<open>
   Global_Theory.add_thms_dynamic (@{binding "mythmlist"}, MyThmList.get) 
-*}
-
-text {*
+\<close>
+
+text \<open>
   with a name and a function that accesses the theorem list. Now if the
   user issues the command
 
   \begin{isabelle}
-  \isacommand{thm}~@{text "mythmlist"}\\
-  @{text "> True"}
+  \isacommand{thm}~\<open>mythmlist\<close>\\
+  \<open>> True\<close>
   \end{isabelle}
 
   the current content of the theorem list is displayed. If more theorems are stored in 
   the list, say
-*}
-
-setup %gray {* update @{thm FalseE} *}
-
-text {*
+\<close>
+
+setup %gray \<open>update @{thm FalseE}\<close>
+
+text \<open>
   then the same command produces
   
   \begin{isabelle}
-  \isacommand{thm}~@{text "mythmlist"}\\
-  @{text "> False \<Longrightarrow> ?P"}\\
-  @{text "> True"}
+  \isacommand{thm}~\<open>mythmlist\<close>\\
+  \<open>> False \<Longrightarrow> ?P\<close>\\
+  \<open>> True\<close>
   \end{isabelle}
 
   Note that if we add the theorem @{thm [source] FalseE} again to the list
-*}
-
-setup %gray {* update @{thm FalseE} *}
-
-text {*
+\<close>
+
+setup %gray \<open>update @{thm FalseE}\<close>
+
+text \<open>
   we still obtain the same list. The reason is that we used the function @{ML_ind
   add_thm in Thm} in our update function. This is a dedicated function which
   tests whether the theorem is already in the list.  This test is done
   according to alpha-equivalence of the proposition of the theorem. The
   corresponding testing function is @{ML_ind eq_thm_prop in Thm}.
   Suppose you proved the following three theorems.
-*}
+\<close>
 
 lemma
   shows thm1: "\<forall>x. P x" 
   and   thm2: "\<forall>y. P y" 
   and   thm3: "\<forall>y. Q y" sorry
 
-text {*
+text \<open>
   Testing them for alpha equality produces:
 
   @{ML_response [display,gray]
@@ -1738,13 +1736,13 @@
 
   Other function produce terms that can be pattern-matched. 
   Suppose the following two theorems.
-*}
+\<close>
 
 lemma  
   shows foo_test1: "A \<Longrightarrow> B \<Longrightarrow> C" 
   and   foo_test2: "A \<longrightarrow> B \<longrightarrow> C" sorry
 
-text {*
+text \<open>
   We can destruct them into premises and conclusions as follows. 
 
  @{ML_response_fake [display,gray]
@@ -1765,8 +1763,8 @@
 Premises: 
 Conclusion: ?A \<longrightarrow> ?B \<longrightarrow> ?C"}
 
-  Note that in the second case, there is no premise. The reason is that @{text "\<Longrightarrow>"}
-  separates premises and conclusion, while @{text "\<longrightarrow>"} is the object implication
+  Note that in the second case, there is no premise. The reason is that \<open>\<Longrightarrow>\<close>
+  separates premises and conclusion, while \<open>\<longrightarrow>\<close> is the object implication
   from HOL, which just constructs a formula.
 
   \begin{readmore}
@@ -1788,8 +1786,8 @@
   "(\<lambda>x. x) = (\<lambda>x. x) \<equiv> (\<lambda>x. x) = (\<lambda>x. x)"}
 
   Often it is necessary to transform theorems to and from the object 
-  logic, that is replacing all @{text "\<longrightarrow>"} and @{text "\<forall>"} by @{text "\<Longrightarrow>"} 
-  and @{text "\<And>"}, or the other way around.  A reason for such a transformation 
+  logic, that is replacing all \<open>\<longrightarrow>\<close> and \<open>\<forall>\<close> by \<open>\<Longrightarrow>\<close> 
+  and \<open>\<And>\<close>, or the other way around.  A reason for such a transformation 
   might be stating a definition. The reason is that definitions can only be 
   stated using object logic connectives, while theorems using the connectives 
   from the meta logic are more convenient for reasoning. Therefore there are
@@ -1822,21 +1820,21 @@
 
   @{thm [display] list.induct}
 
-  we have to first abstract over the meta variables @{text "?P"} and 
-  @{text "?list"}. For this we can use the function 
+  we have to first abstract over the meta variables \<open>?P\<close> and 
+  \<open>?list\<close>. For this we can use the function 
   @{ML_ind forall_intr_vars in Drule}. This allows us to implement the
   following function for atomizing a theorem.
-*}
-
-ML %grayML{*fun atomize_thm ctxt thm =
+\<close>
+
+ML %grayML\<open>fun atomize_thm ctxt thm =
 let
   val thm' = forall_intr_vars thm
   val thm'' = Object_Logic.atomize ctxt (Thm.cprop_of thm')
 in
   Raw_Simplifier.rewrite_rule ctxt [thm''] thm'
-end*}
-
-text {*
+end\<close>
+
+text \<open>
   This function produces for the theorem @{thm [source] list.induct}
 
   @{ML_response_fake [display, gray]
@@ -1859,7 +1857,7 @@
 
   This function takes first a context and second a list of strings. This list
   specifies which variables should be turned into schematic variables once the term
-  is proved (in this case only @{text "\"P\""}).  The fourth argument is the term to be 
+  is proved (in this case only \<open>"P"\<close>).  The fourth argument is the term to be 
   proved. The fifth is a corresponding proof given in form of a tactic (we explain 
   tactics in Chapter~\ref{chp:tactical}). In the code above, the tactic proves the 
   theorem by assumption. 
@@ -1867,16 +1865,16 @@
   There is also the possibility of proving multiple goals at the same time
   using the function @{ML_ind prove_common in Goal}. For this let us define the
   following three helper functions.
-*}
-
-ML %grayML{*fun rep_goals i = replicate i @{prop "f x = f x"}
+\<close>
+
+ML %grayML\<open>fun rep_goals i = replicate i @{prop "f x = f x"}
 fun rep_tacs i = replicate i (resolve_tac @{context} [@{thm refl}])
 
 fun multi_test ctxt i =
   Goal.prove_common ctxt NONE ["f", "x"] [] (rep_goals i) 
-    (K ((Goal.conjunction_tac THEN' RANGE (rep_tacs i)) 1))*}
-
-text {*
+    (K ((Goal.conjunction_tac THEN' RANGE (rep_tacs i)) 1))\<close>
+
+text \<open>
   With them we can now produce three theorem instances of the 
   proposition.
 
@@ -1885,19 +1883,19 @@
   "[\"?f ?x = ?f ?x\", \"?f ?x = ?f ?x\", \"?f ?x = ?f ?x\"]"}
 
   However you should be careful with @{ML prove_common in Goal} and very
-  large goals. If you increase the counter in the code above to @{text 3000}, 
+  large goals. If you increase the counter in the code above to \<open>3000\<close>, 
   you will notice that takes approximately ten(!) times longer than
   using @{ML map} and @{ML prove in Goal}.
-*}
+\<close>
   
-ML %grayML{*let 
+ML %grayML\<open>let 
   fun test_prove ctxt thm =
     Goal.prove ctxt ["P", "x"] [] thm (K (resolve_tac  @{context} [@{thm refl}] 1))
 in
   map (test_prove @{context}) (rep_goals 3000)
-end*}
-
-text {*
+end\<close>
+
+text \<open>
   While the LCF-approach of going through interfaces ensures soundness in Isabelle, there
   is the function @{ML_ind make_thm in Skip_Proof} in the structure 
   @{ML_struct Skip_Proof} that allows us to turn any proposition into a theorem.
@@ -1919,12 +1917,12 @@
   kind, the names for cases and so on. This data is stored in a string-string
   list and can be retrieved with the function @{ML_ind get_tags in
   Thm}. Assume you prove the following lemma.
-*}
+\<close>
 
 lemma foo_data: 
   shows "P \<Longrightarrow> P \<Longrightarrow> P" by assumption
 
-text {*
+text \<open>
   The auxiliary data of this lemma can be retrieved using the function 
   @{ML_ind get_tags in Thm}. So far the the auxiliary data of this lemma is 
 
@@ -1936,14 +1934,14 @@
   we might want to explicitly extend this data by attaching case names to the 
   two premises of the lemma.  This can be done with the function @{ML_ind name in Rule_Cases}
   from the structure @{ML_struct Rule_Cases}.
-*}
-
-local_setup %gray {*
+\<close>
+
+local_setup %gray \<open>
   Local_Theory.note ((@{binding "foo_data'"}, []), 
     [(Rule_Cases.name ["foo_case_one", "foo_case_two"] 
-       @{thm foo_data})]) #> snd *}
-
-text {*
+       @{thm foo_data})]) #> snd\<close>
+
+text \<open>
   The data of the theorem @{thm [source] foo_data'} is then as follows:
 
   @{ML_response_fake [display,gray]
@@ -1952,63 +1950,62 @@
  (\"case_names\", \"foo_case_one;foo_case_two\")]"}
 
   You can observe the case names of this lemma on the user level when using 
-  the proof methods @{text cases} and @{text induct}. In the proof below
-*}
+  the proof methods \<open>cases\<close> and \<open>induct\<close>. In the proof below
+\<close>
 
 lemma
 shows "Q \<Longrightarrow> Q \<Longrightarrow> Q"
 proof (cases rule: foo_data')
 
 (*<*)oops(*>*)
-text_raw{*
+text_raw\<open>
 \begin{tabular}{@ {}l}
 \isacommand{print\_cases}\\
-@{text "> cases:"}\\
-@{text ">   foo_case_one:"}\\
-@{text ">     let \"?case\" = \"?P\""}\\
-@{text ">   foo_case_two:"}\\
-@{text ">     let \"?case\" = \"?P\""}
-\end{tabular}*}
-
-text {*
-  we can proceed by analysing the cases @{text "foo_case_one"} and 
-  @{text "foo_case_two"}. While if the theorem has no names, then
-  the cases have standard names @{text 1}, @{text 2} and so 
+\<open>> cases:\<close>\\
+\<open>>   foo_case_one:\<close>\\
+\<open>>     let "?case" = "?P"\<close>\\
+\<open>>   foo_case_two:\<close>\\
+\<open>>     let "?case" = "?P"\<close>
+\end{tabular}\<close>
+
+text \<open>
+  we can proceed by analysing the cases \<open>foo_case_one\<close> and 
+  \<open>foo_case_two\<close>. While if the theorem has no names, then
+  the cases have standard names \<open>1\<close>, \<open>2\<close> and so 
   on. This can be seen in the proof below.
-*}
+\<close>
 
 lemma
 shows "Q \<Longrightarrow> Q \<Longrightarrow> Q"
 proof (cases rule: foo_data)
 
 (*<*)oops(*>*)
-text_raw{*
+text_raw\<open>
 \begin{tabular}{@ {}l}
 \isacommand{print\_cases}\\
-@{text "> cases:"}\\
-@{text ">   1:"}\\
-@{text ">     let \"?case\" = \"?P\""}\\
-@{text ">   2:"}\\
-@{text ">     let \"?case\" = \"?P\""}
-\end{tabular}*}
+\<open>> cases:\<close>\\
+\<open>>   1:\<close>\\
+\<open>>     let "?case" = "?P"\<close>\\
+\<open>>   2:\<close>\\
+\<open>>     let "?case" = "?P"\<close>
+\end{tabular}\<close>
 
  
-text {*
+text \<open>
   Sometimes one wants to know the theorems that are involved in
-  proving a theorem, especially when the proof is by @{text
-  auto}. These theorems can be obtained by introspecting the proved theorem.
+  proving a theorem, especially when the proof is by \<open>auto\<close>. These theorems can be obtained by introspecting the proved theorem.
   To introspect a theorem, let us define the following three functions
   that analyse the @{ML_type_ind proof_body} data-structure from the
   structure @{ML_struct Proofterm}.
-*}
-
-ML %grayML{*fun pthms_of (PBody {thms, ...}) = map #2 thms 
+\<close>
+
+ML %grayML\<open>fun pthms_of (PBody {thms, ...}) = map #2 thms 
 val get_names = (map Proofterm.thm_node_name) o pthms_of 
-val get_pbodies = map (Future.join o Proofterm.thm_node_body) o pthms_of *}
-
-text {* 
+val get_pbodies = map (Future.join o Proofterm.thm_node_body) o pthms_of\<close>
+
+text \<open>
   To see what their purpose is, consider the following three short proofs.
-*}
+\<close>
 
 lemma my_conjIa:
 shows "A \<and> B \<Longrightarrow> A \<and> B"
@@ -2030,10 +2027,10 @@
 done
 
 
-text {*
+text \<open>
   While the information about which theorems are used is obvious in
   the first two proofs, it is not obvious in the third, because of the
-  @{text auto}-step.  Fortunately, ``behind'' every proved theorem is
+  \<open>auto\<close>-step.  Fortunately, ``behind'' every proved theorem is
   a proof-tree that records all theorems that are employed for
   establishing this theorem.  We can traverse this proof-tree
   extracting this information.  Let us first extract the name of the
@@ -2045,7 +2042,7 @@
   |> get_names"
   "[\"Essential.my_conjIa\"]"}
 
-  whereby @{text "Essential"} refers to the theory name in which
+  whereby \<open>Essential\<close> refers to the theory name in which
   we established the theorem @{thm [source] my_conjIa}. The function @{ML_ind
   proof_body_of in Thm} returns a part of the data that is stored in a
   theorem.  Notice that the first proof above references
@@ -2064,7 +2061,7 @@
 
   The theorems @{thm [source] Pure.protectD} and @{thm [source]
   Pure.protectI} that are internal theorems are always part of a
-  proof in Isabelle. Note also that applications of @{text assumption} do not
+  proof in Isabelle. Note also that applications of \<open>assumption\<close> do not
   count as a separate theorem, as you can see in the following code.
 
   @{ML_response_fake [display,gray]
@@ -2126,54 +2123,54 @@
   styles}}. These are, roughly speaking, functions from terms to terms. The input 
   term stands for the theorem to be presented; the output can be constructed to
   ones wishes.  Let us, for example, assume we want to quote theorems without
-  leading @{text \<forall>}-quantifiers. For this we can implement the following function 
-  that strips off @{text "\<forall>"}s.
-*}
-
-ML %linenosgray{*fun strip_allq (Const (@{const_name "All"}, _) $ Abs body) = 
+  leading \<open>\<forall>\<close>-quantifiers. For this we can implement the following function 
+  that strips off \<open>\<forall>\<close>s.
+\<close>
+
+ML %linenosgray\<open>fun strip_allq (Const (@{const_name "All"}, _) $ Abs body) = 
       Term.dest_abs body |> snd |> strip_allq
   | strip_allq (Const (@{const_name "Trueprop"}, _) $ t) = 
       strip_allq t
-  | strip_allq t = t*}
-
-text {*
+  | strip_allq t = t\<close>
+
+text \<open>
   We use in Line 2 the function @{ML_ind dest_abs in Term} for deconstructing abstractions,
   since this function deals correctly with potential name clashes. This function produces
   a pair consisting of the variable and the body of the abstraction. We are only interested
   in the body, which we feed into the recursive call. In Line 3 and 4, we also
   have to explicitly strip of the outermost @{term Trueprop}-coercion. Now we can 
-  install this function as the theorem style named @{text "my_strip_allq"}. 
-*}
-
-setup %gray{* 
+  install this function as the theorem style named \<open>my_strip_allq\<close>. 
+\<close>
+
+setup %gray\<open>
   Term_Style.setup @{binding "my_strip_allq"} (Scan.succeed (K strip_allq)) 
-*}
-
-text {*
+\<close>
+
+text \<open>
   We can test this theorem style with the following theorem
-*}
+\<close>
 
 theorem style_test:
 shows "\<forall>x y z. (x, x) = (y, z)" sorry
 
-text {*
+text \<open>
   Now printing out in a document the theorem @{thm [source] style_test} normally
-  using @{text "@{thm \<dots>}"} produces
+  using \<open>@{thm \<dots>}\<close> produces
 
   \begin{isabelle}
   \begin{graybox}
-  @{text "@{thm style_test}"}\\
-  @{text ">"}~@{thm style_test}
+  \<open>@{thm style_test}\<close>\\
+  \<open>>\<close>~@{thm style_test}
   \end{graybox}
   \end{isabelle}
 
-  as expected. But with the theorem style @{text "@{thm (my_strip_allq) \<dots>}"} 
+  as expected. But with the theorem style \<open>@{thm (my_strip_allq) \<dots>}\<close> 
   we obtain
 
   \begin{isabelle}
   \begin{graybox}
-  @{text "@{thm (my_strip_allq) style_test}"}\\
-  @{text ">"}~@{thm (my_strip_allq) style_test}
+  \<open>@{thm (my_strip_allq) style_test}\<close>\\
+  \<open>>\<close>~@{thm (my_strip_allq) style_test}
   \end{graybox}
   \end{isabelle}
   
@@ -2181,43 +2178,43 @@
   giving a list of strings that should be used for the replacement of the
   variables. For this we implement the function which takes a list of strings
   and uses them as name in the outermost abstractions.
-*}
-
-ML %grayML{*fun rename_allq [] t = t
+\<close>
+
+ML %grayML\<open>fun rename_allq [] t = t
   | rename_allq (x::xs) (Const (@{const_name "All"}, U) $ Abs (_, T, t)) = 
       Const (@{const_name "All"}, U) $ Abs (x, T, rename_allq xs t)
   | rename_allq xs (Const (@{const_name "Trueprop"}, U) $ t) =
       rename_allq xs t
-  | rename_allq _ t = t*}
-
-text {*
+  | rename_allq _ t = t\<close>
+
+text \<open>
   We can now install a the modified theorem style as follows
-*}
-
-setup %gray {* let
+\<close>
+
+setup %gray \<open>let
   val parser = Scan.repeat Args.name
   fun action xs = K (rename_allq xs #> strip_allq)
 in
   Term_Style.setup @{binding "my_strip_allq2"} (parser >> action)
-end *}
-
-text {*
-  The parser reads a list of names. In the function @{text action} we first
+end\<close>
+
+text \<open>
+  The parser reads a list of names. In the function \<open>action\<close> we first
   call @{ML rename_allq} with the parsed list, then we call @{ML strip_allq}
   on the resulting term. We can now suggest, for example, two variables for
-  stripping off the first two @{text \<forall>}-quantifiers.
+  stripping off the first two \<open>\<forall>\<close>-quantifiers.
 
   \begin{isabelle}
   \begin{graybox}
-  @{text "@{thm (my_strip_allq2 x' x'') style_test}"}\\
-  @{text ">"}~@{thm (my_strip_allq2 x' x'') style_test}
+  \<open>@{thm (my_strip_allq2 x' x'') style_test}\<close>\\
+  \<open>>\<close>~@{thm (my_strip_allq2 x' x'') style_test}
   \end{graybox}
   \end{isabelle}
 
   Such styles allow one to print out theorems in documents formatted to 
   ones heart content. The styles can also be used in the document 
-  antiquotations @{text "@{prop ...}"}, @{text "@{term_type ...}"}
-  and @{text "@{typeof ...}"}.
+  antiquotations \<open>@{prop ...}\<close>, \<open>@{term_type ...}\<close>
+  and \<open>@{typeof ...}\<close>.
 
   Next we explain theorem attributes, which is another
   mechanism for dealing with theorems.
@@ -2225,13 +2222,12 @@
   \begin{readmore}
   Theorem styles are implemented in @{ML_file "Pure/Thy/term_style.ML"}.
   \end{readmore}
-*}
-
-section {* Theorem Attributes\label{sec:attributes} *}
-
-text {*
-  Theorem attributes are @{text "[symmetric]"}, @{text "[THEN \<dots>]"}, @{text
-  "[simp]"} and so on. Such attributes are \emph{neither} tags \emph{nor} flags
+\<close>
+
+section \<open>Theorem Attributes\label{sec:attributes}\<close>
+
+text \<open>
+  Theorem attributes are \<open>[symmetric]\<close>, \<open>[THEN \<dots>]\<close>, \<open>[simp]\<close> and so on. Such attributes are \emph{neither} tags \emph{nor} flags
   annotated to theorems, but functions that do further processing of 
   theorems. In particular, it is not possible to find out
   what are all theorems that have a given attribute in common, unless of course
@@ -2243,121 +2239,121 @@
 
   \begin{isabelle}
   \isacommand{print\_attributes}\\
-  @{text "> COMP:  direct composition with rules (no lifting)"}\\
-  @{text "> HOL.dest:  declaration of Classical destruction rule"}\\
-  @{text "> HOL.elim:  declaration of Classical elimination rule"}\\
-  @{text "> \<dots>"}
+  \<open>> COMP:  direct composition with rules (no lifting)\<close>\\
+  \<open>> HOL.dest:  declaration of Classical destruction rule\<close>\\
+  \<open>> HOL.elim:  declaration of Classical elimination rule\<close>\\
+  \<open>> \<dots>\<close>
   \end{isabelle}
   
   The theorem attributes fall roughly into two categories: the first category manipulates
-  theorems (for example @{text "[symmetric]"} and @{text "[THEN \<dots>]"}), and the second
-  stores theorems somewhere as data (for example @{text "[simp]"}, which adds
+  theorems (for example \<open>[symmetric]\<close> and \<open>[THEN \<dots>]\<close>), and the second
+  stores theorems somewhere as data (for example \<open>[simp]\<close>, which adds
   theorems to the current simpset).
 
   To explain how to write your own attribute, let us start with an extremely simple 
-  version of the attribute @{text "[symmetric]"}. The purpose of this attribute is
+  version of the attribute \<open>[symmetric]\<close>. The purpose of this attribute is
   to produce the ``symmetric'' version of an equation. The main function behind 
   this attribute is
-*}
-
-ML %grayML{*val my_symmetric = Thm.rule_attribute [] (fn _ => fn thm => thm RS @{thm sym})*}
-
-text {* 
+\<close>
+
+ML %grayML\<open>val my_symmetric = Thm.rule_attribute [] (fn _ => fn thm => thm RS @{thm sym})\<close>
+
+text \<open>
   where the function @{ML_ind  rule_attribute in Thm} expects a function taking a 
-  context (which we ignore in the code above) and a theorem (@{text thm}), and 
-  returns another theorem (namely @{text thm} resolved with the theorem 
+  context (which we ignore in the code above) and a theorem (\<open>thm\<close>), and 
+  returns another theorem (namely \<open>thm\<close> resolved with the theorem 
   @{thm [source] sym}: @{thm sym[no_vars]}; the function @{ML_ind RS in Drule} 
   is explained in Section~\ref{sec:simpletacs}). The function 
   @{ML rule_attribute in Thm} then returns  an attribute.
 
   Before we can use the attribute, we need to set it up. This can be done
   using the Isabelle command \isacommand{attribute\_setup} as follows:
-*}
+\<close>
 
 attribute_setup %gray my_sym = 
-  {* Scan.succeed my_symmetric *} "applying the sym rule"
-
-text {*
-  Inside the @{text "\<verbopen> \<dots> \<verbclose>"}, we have to specify a parser
+  \<open>Scan.succeed my_symmetric\<close> "applying the sym rule"
+
+text \<open>
+  Inside the \<open>\<verbopen> \<dots> \<verbclose>\<close>, we have to specify a parser
   for the theorem attribute. Since the attribute does not expect any further 
-  arguments (unlike @{text "[THEN \<dots>]"}, for instance), we use the parser @{ML
-  Scan.succeed}. An example for the attribute @{text "[my_sym]"} is the proof
-*} 
+  arguments (unlike \<open>[THEN \<dots>]\<close>, for instance), we use the parser @{ML
+  Scan.succeed}. An example for the attribute \<open>[my_sym]\<close> is the proof
+\<close> 
 
 lemma test[my_sym]: "2 = Suc (Suc 0)" by simp
 
-text {*
+text \<open>
   which stores the theorem @{thm test} under the name @{thm [source] test}. You
   can see this, if you query the lemma: 
 
   \begin{isabelle}
-  \isacommand{thm}~@{text "test"}\\
-  @{text "> "}~@{thm test}
+  \isacommand{thm}~\<open>test\<close>\\
+  \<open>> \<close>~@{thm test}
   \end{isabelle}
 
   We can also use the attribute when referring to this theorem:
 
   \begin{isabelle}
-  \isacommand{thm}~@{text "test[my_sym]"}\\
-  @{text "> "}~@{thm test[my_sym]}
+  \isacommand{thm}~\<open>test[my_sym]\<close>\\
+  \<open>> \<close>~@{thm test[my_sym]}
   \end{isabelle}
 
   An alternative for setting up an attribute is the function @{ML_ind  setup in Attrib}.
   So instead of using \isacommand{attribute\_setup}, you can also set up the
   attribute as follows:
-*}
-
-ML %grayML{*Attrib.setup @{binding "my_sym"} (Scan.succeed my_symmetric)
-  "applying the sym rule" *}
-
-text {*
+\<close>
+
+ML %grayML\<open>Attrib.setup @{binding "my_sym"} (Scan.succeed my_symmetric)
+  "applying the sym rule"\<close>
+
+text \<open>
   This gives a function from @{ML_type "theory -> theory"}, which
   can be used for example with \isacommand{setup} or with
   @{ML "Context.>> o Context.map_theory"}.\footnote{\bf FIXME: explain what happens here.}
 
   As an example of a slightly more complicated theorem attribute, we implement 
-  our own version of @{text "[THEN \<dots>]"}. This attribute will take a list of theorems
+  our own version of \<open>[THEN \<dots>]\<close>. This attribute will take a list of theorems
   as argument and resolve the theorem with this list (one theorem 
   after another). The code for this attribute is
-*}
-
-ML %grayML{*fun MY_THEN thms = 
+\<close>
+
+ML %grayML\<open>fun MY_THEN thms = 
 let
   fun RS_rev thm1 thm2 = thm2 RS thm1
 in
   Thm.rule_attribute [] (fn _ => fn thm => fold RS_rev thms thm)
-end*}
-
-text {* 
+end\<close>
+
+text \<open>
   where for convenience we define the reverse and curried version of @{ML RS}. 
   The setup of this theorem attribute uses the parser @{ML thms in Attrib}, 
   which parses a list of theorems. 
-*}
-
-attribute_setup %gray MY_THEN = {* Attrib.thms >> MY_THEN *} 
+\<close>
+
+attribute_setup %gray MY_THEN = \<open>Attrib.thms >> MY_THEN\<close> 
   "resolving the list of theorems with the theorem"
 
-text {* 
+text \<open>
   You can, for example, use this theorem attribute to turn an equation into a 
   meta-equation:
 
   \begin{isabelle}
-  \isacommand{thm}~@{text "test[MY_THEN eq_reflection]"}\\
-  @{text "> "}~@{thm test[MY_THEN eq_reflection]}
+  \isacommand{thm}~\<open>test[MY_THEN eq_reflection]\<close>\\
+  \<open>> \<close>~@{thm test[MY_THEN eq_reflection]}
   \end{isabelle}
 
   If you need the symmetric version as a meta-equation, you can write
 
   \begin{isabelle}
-  \isacommand{thm}~@{text "test[MY_THEN sym eq_reflection]"}\\
-  @{text "> "}~@{thm test[MY_THEN sym eq_reflection]}
+  \isacommand{thm}~\<open>test[MY_THEN sym eq_reflection]\<close>\\
+  \<open>> \<close>~@{thm test[MY_THEN sym eq_reflection]}
   \end{isabelle}
 
   It is also possible to combine different theorem attributes, as in:
   
   \begin{isabelle}
-  \isacommand{thm}~@{text "test[my_sym, MY_THEN eq_reflection]"}\\
-  @{text "> "}~@{thm test[my_sym, MY_THEN eq_reflection]}
+  \isacommand{thm}~\<open>test[my_sym, MY_THEN eq_reflection]\<close>\\
+  \<open>> \<close>~@{thm test[my_sym, MY_THEN eq_reflection]}
   \end{isabelle}
   
   However, here also a weakness of the concept
@@ -2365,8 +2361,8 @@
   arbitrary functions, they do not commute in general. If you try
 
   \begin{isabelle}
-  \isacommand{thm}~@{text "test[MY_THEN eq_reflection, my_sym]"}\\
-  @{text "> "}~@{text "exception THM 1 raised: RSN: no unifiers"}
+  \isacommand{thm}~\<open>test[MY_THEN eq_reflection, my_sym]\<close>\\
+  \<open>> \<close>~\<open>exception THM 1 raised: RSN: no unifiers\<close>
   \end{isabelle}
 
   you get an exception indicating that the theorem @{thm [source] sym}
@@ -2374,42 +2370,42 @@
 
   The purpose of @{ML_ind rule_attribute in Thm} is to directly manipulate
   theorems.  Another usage of theorem attributes is to add and delete theorems
-  from stored data.  For example the theorem attribute @{text "[simp]"} adds
+  from stored data.  For example the theorem attribute \<open>[simp]\<close> adds
   or deletes a theorem from the current simpset. For these applications, you
   can use @{ML_ind declaration_attribute in Thm}. To illustrate this function,
   let us introduce a theorem list.
-*}
-
-ML %grayML{*structure MyThms = Named_Thms
+\<close>
+
+ML %grayML\<open>structure MyThms = Named_Thms
   (val name = @{binding "attr_thms"} 
-   val description = "Theorems for an Attribute") *}
-
-text {* 
+   val description = "Theorems for an Attribute")\<close>
+
+text \<open>
   We are going to modify this list by adding and deleting theorems.
   For this we use the two functions @{ML MyThms.add_thm} and
   @{ML MyThms.del_thm}. You can turn them into attributes 
   with the code
-*}
-
-ML %grayML{*val my_add = Thm.declaration_attribute MyThms.add_thm
-val my_del = Thm.declaration_attribute MyThms.del_thm *}
-
-text {* 
+\<close>
+
+ML %grayML\<open>val my_add = Thm.declaration_attribute MyThms.add_thm
+val my_del = Thm.declaration_attribute MyThms.del_thm\<close>
+
+text \<open>
   and set up the attributes as follows
-*}
-
-attribute_setup %gray my_thms = {* Attrib.add_del my_add my_del *} 
+\<close>
+
+attribute_setup %gray my_thms = \<open>Attrib.add_del my_add my_del\<close> 
   "maintaining a list of my_thms" 
 
-text {*
+text \<open>
   The parser @{ML_ind  add_del in Attrib} is a predefined parser for 
   adding and deleting lemmas. Now if you prove the next lemma 
-  and attach to it the attribute @{text "[my_thms]"}
-*}
+  and attach to it the attribute \<open>[my_thms]\<close>
+\<close>
 
 lemma trueI_2[my_thms]: "True" by simp
 
-text {*
+text \<open>
   then you can see it is added to the initially empty list.
 
   @{ML_response_fake [display,gray]
@@ -2417,12 +2413,12 @@
   "[\"True\"]"}
 
   You can also add theorems using the command \isacommand{declare}.
-*}
+\<close>
 
 declare test[my_thms] trueI_2[my_thms add]
 
-text {*
-  With this attribute, the @{text "add"} operation is the default and does 
+text \<open>
+  With this attribute, the \<open>add\<close> operation is the default and does 
   not need to be explicitly given. These three declarations will cause the 
   theorem list to be updated as:
 
@@ -2433,11 +2429,11 @@
   The theorem @{thm [source] trueI_2} only appears once, since the 
   function @{ML_ind  add_thm in Thm} tests for duplicates, before extending
   the list. Deletion from the list works as follows:
-*}
+\<close>
 
 declare test[my_thms del]
 
-text {* After this, the theorem list is again: 
+text \<open>After this, the theorem list is again: 
 
   @{ML_response_fake [display,gray]
   "MyThms.get @{context}"
@@ -2447,7 +2443,7 @@
   declaration_attribute in Thm}, but there can be any number of them. We just
   have to change the parser for reading the arguments accordingly.
 
-  \footnote{\bf FIXME What are: @{text "theory_attributes"}, @{text "proof_attributes"}?}
+  \footnote{\bf FIXME What are: \<open>theory_attributes\<close>, \<open>proof_attributes\<close>?}
   \footnote{\bf FIXME readmore}
 
   \begin{readmore}
@@ -2455,11 +2451,11 @@
   @{ML_file "Pure/Isar/attrib.ML"}...also explained in the chapter about
   parsing.
   \end{readmore}
-*}
-
-section {* Pretty-Printing\label{sec:pretty} *}
-
-text {*
+\<close>
+
+section \<open>Pretty-Printing\label{sec:pretty}\<close>
+
+text \<open>
   So far we printed out only plain strings without any formatting except for
   occasional explicit line breaks using @{text [quotes] "\\n"}. This is
   sufficient for ``quick-and-dirty'' printouts. For something more
@@ -2483,26 +2479,26 @@
   string}. This can be done with the function @{ML_ind  string_of in Pretty}. In what
   follows we will use the following wrapper function for printing a pretty
   type:
-*}
-
-ML %grayML{*fun pprint prt = tracing (Pretty.string_of prt)*}
-
-text {*
+\<close>
+
+ML %grayML\<open>fun pprint prt = tracing (Pretty.string_of prt)\<close>
+
+text \<open>
   The point of the pretty-printing infrastructure is to give hints about how to
   layout text and let Isabelle do the actual layout. Let us first explain
   how you can insert places where a line break can occur. For this assume the
   following function that replicates a string n times:
-*}
-
-ML %grayML{*fun rep n str = implode (replicate n str) *}
-
-text {*
+\<close>
+
+ML %grayML\<open>fun rep n str = implode (replicate n str)\<close>
+
+text \<open>
   and suppose we want to print out the string:
-*}
-
-ML %grayML{*val test_str = rep 8 "fooooooooooooooobaaaaaaaaaaaar "*}
-
-text {*
+\<close>
+
+ML %grayML\<open>val test_str = rep 8 "fooooooooooooooobaaaaaaaaaaaar "\<close>
+
+text \<open>
   We deliberately chose a large string so that it spans over more than one line. 
   If we print out the string using the usual ``quick-and-dirty'' method, then
   we obtain the ugly output:
@@ -2590,9 +2586,9 @@
   list as a ``set'', that means enclosed inside @{text [quotes] "{"} and
   @{text [quotes] "}"}, and separated by commas using the function
   @{ML_ind  enum in Pretty}. For example
-*}
-
-text {*
+\<close>
+
+text \<open>
   
 @{ML_response_fake [display,gray]
 "let
@@ -2613,9 +2609,9 @@
   the last two items are separated by @{text [quotes] "and"}. For this you can
   write the function
 
-*}
-
-ML %linenosgray{*fun and_list [] = []
+\<close>
+
+ML %linenosgray\<open>fun and_list [] = []
   | and_list [x] = [x]
   | and_list xs = 
       let 
@@ -2623,9 +2619,9 @@
       in
         (Pretty.commas front) @ 
         [Pretty.brk 1, Pretty.str "and", Pretty.brk 1, last]
-      end *}
-
-text {*
+      end\<close>
+
+text \<open>
   where Line 7 prints the beginning of the list and Line
   8 the last item. We have to use @{ML "Pretty.brk 1"} in order
   to insert a space (of length 1) before the 
@@ -2695,10 +2691,10 @@
 
   We use the function @{ML_ind pretty_term in Syntax} for pretty-printing
   terms. Next we like to pretty-print a term and its type. For this we use the
-  function @{text "tell_type"}.
-*}
-
-ML %linenosgray{*fun tell_type ctxt trm = 
+  function \<open>tell_type\<close>.
+\<close>
+
+ML %linenosgray\<open>fun tell_type ctxt trm = 
 let
   fun pstr s = Pretty.breaks (map Pretty.str (space_explode " " s))
   val ptrm = Pretty.quote (Syntax.pretty_term ctxt trm)
@@ -2707,9 +2703,9 @@
   pprint (Pretty.blk (0, 
     (pstr "The term " @ [ptrm] @ pstr " has type " 
       @ [pty, Pretty.str "."])))
-end*}
-
-text {*
+end\<close>
+
+text \<open>
   In Line 3 we define a function that inserts possible linebreaks in places
   where a space is. In Lines 4 and 5 we pretty-print the term and its type
   using the functions @{ML pretty_term in Syntax} and @{ML_ind 
@@ -2738,17 +2734,17 @@
   
   @{ML_file "Pure/PIDE/markup.ML"}
   \end{readmore}
-*}
-
-section {* Summary *}
-
-text {*
+\<close>
+
+section \<open>Summary\<close>
+
+text \<open>
   \begin{conventions}
   \begin{itemize}
   \item Start with a proper context and then pass it around 
   through all your functions.
   \end{itemize}
   \end{conventions}
-*}
+\<close>
 
 end




