isabelle-cookbook: comparison ProgTutorial/Essential.thy

equal deleted inserted replaced

-:6e2479089226
+:cecd7a941885
 theory Essential
 imports Base First_Steps
 begin
-chapter {* Isabelle Essentials *}
+chapter \<open>Isabelle Essentials\<close>
-text {*
+text \<open>
 \begin{flushright}
 {\em One man's obfuscation is another man's abstraction.} \\[1ex]
 Frank Ch.~Eigler on the Linux Kernel Mailing List,\\
 24~Nov.~2009
 \end{flushright}
 Isabelle is built around a few central ideas. One central idea is the
 LCF-approach to theorem proving \cite{GordonMilnerWadsworth79} where there
 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.
-*}
+\<close>
-section {* Terms and Types *}
+section \<open>Terms and Types\<close>
-text {*
+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\"}"
 "Const (\"HOL.eq\", \<dots>) $
 (Const (\"Groups.plus_class.plus\", \<dots>) $ \<dots> $ \<dots>) $ \<dots>"}
 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:
-*}
+\<close>
-ML_val %linenosgray{*datatype term =
+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 *}
+| $ of term * term\<close>
-text {*
+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;
 this cannot be done with certified terms. As can be seen in Line 5,
 terms use the usual de Bruijn index mechanism for representing bound
 end"
 "?x3, ?x1.3, x"}
 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
+variables using the built-in antiquotation \mbox{\<open>@{term
-\<dots>}"}}). If you deal with theorems, you have to, however, observe the
+\<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
 (see below).
 Hint: The third term is already quite big, and the pretty printer
 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 {*
+text \<open>
-The antiquotation @{text "@{prop \<dots>}"} constructs terms by inserting the
+The antiquotation \<open>@{prop \<dots>}\<close> constructs terms by inserting the
-usually invisible @{text "Trueprop"}-coercions whenever necessary.
+usually invisible \<open>Trueprop\<close>-coercions whenever necessary.
 Consider for example the pairs
 @{ML_response [display,gray] "(@{term \"P x\"}, @{prop \"P x\"})"
 "(Free (\"P\", \<dots>) $ Free (\"x\", \<dots>),
 Const (\"HOL.Trueprop\", \<dots>) $ (Free (\"P\", \<dots>) $ Free (\"x\", \<dots>)))"}
 @{ML_response [display,gray] "(@{term \"P x \<Longrightarrow> Q x\"}, @{prop \"P x \<Longrightarrow> Q x\"})"
 "(Const (\"Pure.imp\", \<dots>) $ \<dots> $ \<dots>,
 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 *}
+| TVar  of indexname * sort\<close>
-text {*
+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
 a leading question mark). A type constant,
 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
+which is the pretty printed version of \<open>bool\<close>. However, in PolyML
-(version @{text "\<ge>"}5.3) it is easy to install your own pretty printer. With the
+(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}).
-*}
+\<close>
-ML %grayML{*local
+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
 fun pp_qstr s  = Pretty.quote (pp_str s)
 fun pp_int i   = pp_str (string_of_int i)
 pp_constr "TVar" (pp_pair (pp_pair (pp_qstr a, pp_int i), pp_sort S))
 | raw_pp_typ (TFree (a, S)) =
 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*}
+end\<close>
-text {*
+text \<open>
 We can install this pretty printer with the function
 @{ML_ind ML_system_pp} as follows.
-*}
+\<close>
-ML %grayML{*ML_system_pp
+ML %grayML\<open>ML_system_pp
-(fn _ => fn _ => Pretty.to_polyml o raw_pp_typ)*}
+(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]
 "@{typ \"bool\"}"
 "Type (\"HOL.bool\", [])"}
 @{ML_response [display,gray]
 "@{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
+we can see the full name of the type is actually \<open>List.list\<close>, indicating
-that it is defined in the theory @{text "List"}. However, one has to be
+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]
 "@{typ \"bool \<Rightarrow> nat\"}"
 "Type (\"fun\", [Type (\"HOL.bool\", []), Type (\"Nat.nat\", [])])"}
 We can restore the usual behaviour of Isabelle's pretty printer
 with the code
-*}
+\<close>
-ML %grayML{*ML_system_pp
+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)*}
+(fn depth => fn _ => ML_Pretty.to_polyml o Pretty.to_ML depth o Proof_Display.pp_typ Theory.get_pure)\<close>
-text {*
+text \<open>
 After that the types for booleans, lists and so on are printed out again
 the standard Isabelle way.
 @{ML_response_fake [display, gray]
 "@{typ \"bool\"};
 \begin{readmore}
 Types are described in detail in \isccite{sec:types}. Their
 definition and many useful operations are implemented
 in @{ML_file "Pure/type.ML"}.
 \end{readmore}
-*}
+\<close>
-section {* Constructing Terms and Types Manually\label{sec:terms_types_manually} *}
+section \<open>Constructing Terms and Types Manually\label{sec:terms_types_manually}\<close>
-text {*
+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:
-*}
+\<close>
-ML %grayML{*fun make_imp P Q =
+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 *}
+end\<close>
-text {*
+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.
-*}
+\<close>
-ML %grayML{*fun make_wrong_imp P Q = @{prop "\<And>(x::nat). P x \<Longrightarrow> Q x"} *}
+ML %grayML\<open>fun make_wrong_imp P Q = @{prop "\<And>(x::nat). P x \<Longrightarrow> Q x"}\<close>
-text {*
+text \<open>
-To see this, apply @{text "@{term S}"} and @{text "@{term T}"}
+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
 @{ML_response [display,gray] "make_imp @{term S} @{term T}"
 "Const \<dots> $
 Abs (\"x\", Type (\"Nat.nat\",[]),
 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> $
 Abs (\"x\", \<dots>,
 Const \<dots> $ (Const \<dots> $ (Free (\"P\",\<dots>) $ \<dots>)) $
 "Abs (\"x\", \"Nat.nat\", Free (\"P\", \"bool \<Rightarrow> bool\") $ Bound 0)"}
 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
 @{ML_response_fake [display,gray]
 "let
 in
 lambda x_int trm
 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.
 There is also the function @{ML_ind subst_free in Term} with which terms can be
 "Free (\"x\", \"nat\")"}
 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.
-*}
+\<close>
-ML %grayML{*fun strip_alls t =
+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*}
+end\<close>
-text {*
+text \<open>
 The function returns a pair consisting of the stripped off variables and
 the body of the universal quantification. For example
 @{ML_response_fake [display, gray]
 "strip_alls @{term \"\<forall>x y. x = (y::bool)\"}"
 Const (\"op =\", \<dots>) $ Bound 1 $ Bound 0)"}
 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))*}
+$ Abs (x, T, build_alls (vs, t))\<close>
-text {*
+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.
 @{ML_response_fake [display, gray, linenos]
 \end{readmore}
 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
+\<open>is_true\<close> as follows
-*}
+\<close>
-ML %grayML{*fun is_true @{term True} = true
+ML %grayML\<open>fun is_true @{term True} = true
-| is_true _ = false*}
+| is_true _ = false\<close>
-text {*
+text \<open>
-this does not work for picking out @{text "\<forall>"}-quantified terms. Because
+this does not work for picking out \<open>\<forall>\<close>-quantified terms. Because
 the function
-*}
+\<close>
-ML %grayML{*fun is_all (@{term All} $ _) = true
+ML %grayML\<open>fun is_all (@{term All} $ _) = true
-| is_all _ = false*}
+| is_all _ = false\<close>
-text {*
+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
-*}
+\<close>
-ML %grayML{*fun is_all (Const ("HOL.All", _) $ _) = true
+ML %grayML\<open>fun is_all (Const ("HOL.All", _) $ _) = true
-| is_all _ = false*}
+| is_all _ = false\<close>
-text {*
+text \<open>
 because now
 @{ML_response [display,gray] "is_all @{term \"\<forall>x::nat. P x\"}" "true"}
 matches correctly (the first wildcard in the pattern matches any type and the
 second any term).
 However there is still a problem: consider the similar function that
-attempts to pick out @{text "Nil"}-terms:
+attempts to pick out \<open>Nil\<close>-terms:
-*}
+\<close>
-ML %grayML{*fun is_nil (Const ("Nil", _)) = true
+ML %grayML\<open>fun is_nil (Const ("Nil", _)) = true
-| is_nil _ = false *}
+| is_nil _ = false\<close>
-text {*
+text \<open>
 Unfortunately, also this function does \emph{not} work as expected, since
 @{ML_response [display,gray] "is_nil @{term \"Nil\"}" "false"}
 The problem is that on the ML-level the name of a constant is more
 because @{term "All"} is such a fundamental constant, which can be referenced
 by @{ML "Const (\"All\", some_type)" for some_type}. However, if you look at
 @{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
+the name of the constant \<open>Nil\<close> depends on the theory in which the
-term constructor is defined (@{text "List"}) and also in which datatype
+term constructor is defined (\<open>List\<close>) and also in which datatype
-(@{text "list"}). Even worse, some constants have a name involving
+(\<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"}}:
 @{ML_response [display,gray] "(@{term \"0::nat\"}, @{term \"times\"})"
 "(Const (\"Groups.zero_class.zero\", \<dots>),
 Const (\"Groups.times_class.times\", \<dots>))"}
 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.
-*}
+\<close>
-ML %grayML{*fun is_nil_or_all (Const (@{const_name "Nil"}, _)) = true
+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 *}
+| is_nil_or_all _ = false\<close>
-text {*
+text \<open>
-The antiquotation for properly referencing type constants is @{text "@{type_name \<dots>}"}.
+The antiquotation for properly referencing type constants is \<open>@{type_name \<dots>}\<close>.
 For example
 @{ML_response [display,gray]
 "@{type_name \"list\"}" "\"List.list\""}
 Although types of terms can often be inferred, there are many
 situations where you need to construct types manually, especially
 when defining constants. For example the function returning a function
 type is as follows:
-*}
+\<close>
-ML %grayML{*fun make_fun_type ty1 ty2 = Type ("fun", [ty1, ty2]) *}
+ML %grayML\<open>fun make_fun_type ty1 ty2 = Type ("fun", [ty1, ty2])\<close>
-text {* This can be equally written with the combinator @{ML_ind "-->" in Term} as: *}
+text \<open>This can be equally written with the combinator @{ML_ind "-->" in Term} as:\<close>
-ML %grayML{*fun make_fun_type ty1 ty2 = ty1 --> ty2 *}
+ML %grayML\<open>fun make_fun_type ty1 ty2 = ty1 --> ty2\<close>
-text {*
+text \<open>
 If you want to construct a function type with more than one argument
 type, then you can use @{ML_ind "--->" in Term}.
-*}
+\<close>
-ML %grayML{*fun make_fun_types tys ty = tys ---> ty *}
+ML %grayML\<open>fun make_fun_types tys ty = tys ---> ty\<close>
-text {*
+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:
-*}
+\<close>
-ML %grayML{*fun nat_to_int ty =
+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)*}
+| _ => ty)\<close>
-text {*
+text \<open>
 Here is an example:
 @{ML_response_fake [display,gray]
 "map_types nat_to_int @{term \"a = (1::nat)\"}"
 "Const (\"op =\", \"int \<Rightarrow> int \<Rightarrow> bool\")
 "Term.add_tfrees @{term \"(a, b)\"} []"
 "[(\"'b\", [\"HOL.type\"]), (\"'a\", [\"HOL.type\"])]"}
 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
+Write a function \<open>rev_sum : term -> term\<close> that takes a
-term of the form @{text "t\<^sub>1 + t\<^sub>2 + \<dots> + t\<^sub>n"} (whereby @{text "n"} might be one)
+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 @{text "t\<^sub>n + \<dots> + t\<^sub>2 + t\<^sub>1"}. Assume
+and returns the reversed sum \<open>t\<^sub>n + \<dots> + t\<^sub>2 + t\<^sub>1\<close>. Assume
-the @{text "t\<^sub>i"} can be arbitrary expressions and also note that @{text "+"}
+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}
 \begin{exercise}\label{fun:makesum}
 Write a function that takes two terms representing natural numbers
 quantification @{term "y"}. Hint: use the functions @{ML incr_boundvars}
 and @{ML loose_bvar1}.
 \end{exercise}
 \begin{exercise}\label{fun:makelist}
-Write a function that takes an integer @{text i} and
+Write a function that takes an integer \<open>i\<close> and
-produces an Isabelle integer list from @{text 1} upto @{text i},
+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}.
 \end{exercise}
 Make sure you use the functions defined in @{ML_file "HOL/Tools/hologic.ML"}
 for constructing the terms for the logical connectives.\footnote{Thanks to Roy
 Dyckhoff for suggesting this exercise and working out the details.}
 \end{exercise}
-*}
+\<close>
-section {* Unification and Matching\label{sec:univ} *}
+section \<open>Unification and Matching\label{sec:univ}\<close>
-text {*
+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
 more concrete by instantiations. Such instantiations might be a result of
 unification or matching. While in case of types, unification and matching is
 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.
 Let us begin with describing the unification and matching functions for
 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 *
+for unifying the types \<open>?'a * ?'b\<close> and \<open>?'b list *
-nat"}. This will produce the mapping, or type environment, @{text "[?'a :=
+nat\<close>. This will produce the mapping, or type environment, \<open>[?'a :=
-?'b list, ?'b := nat]"}.
+?'b list, ?'b := nat]\<close>.
-*}
+\<close>
-ML %linenosgray{*val (tyenv_unif, _) = let
+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*}
+end\<close>
-text {*
+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}.
 @{ML_response_fake [display,gray]
 "Vartab.dest tyenv_unif"
 "[((\"'a\", 0), ([\"HOL.type\"], \"?'b List.list\")),
 ((\"'b\", 0), ([\"HOL.type\"], \"nat\"))]"}
-*}
+\<close>
-text_raw {*
+text_raw \<open>
 \begin{figure}[t]
 \begin{minipage}{\textwidth}
-\begin{isabelle}*}
+\begin{isabelle}\<close>
-ML %grayML{*fun pretty_helper aux env =
+ML %grayML\<open>fun pretty_helper aux env =
 env |> Vartab.dest
 |> map aux
 |> map (fn (s1, s2) => Pretty.block [s1, Pretty.str " := ", s2])
 |> Pretty.enum "," "[" "]"
 |> pwriteln
 let
 fun get_typs (v, (s, T)) = (TVar (v, s), T)
 val print = apply2 (pretty_typ ctxt)
 in
 pretty_helper (print o get_typs) tyenv
-end*}
+end\<close>
-text_raw {*
+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}
-*}
+\<close>
-text {*
+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:
 "[?'a := ?'b list, ?'b := nat]"}
 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
-*}
+\<close>
-ML %linenosgray{*val (tyenvs, _) = let
+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*}
+end\<close>
-text {*
+text \<open>
-The index @{text 0} in Line 5 is the maximal index of the schematic type
+The index \<open>0\<close> in Line 5 is the maximal index of the schematic type
-variables occurring in @{text tys1} and @{text tys2}. This index will be
+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
+say \<open>s1\<close> and \<open>s2\<close>, which we attach to the schematic type
-variables @{text "?'a"} and @{text "?'b"}. Since we do not make any
+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*}
+end\<close>
-text {*
+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.
 @{ML_response_fake [display,gray]
 "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
+As can be seen, the type variables \<open>?'a\<close> and \<open>?'b\<close> are instantiated
-with a new type variable @{text "?'a1"} with sort @{text "{s1, s2}"}. Since a new
+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 @{text 0},
+type variable has been introduced the @{ML index}, originally being \<open>0\<close>,
-has been increased to @{text 1}.
+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
+Let us now return to the unification problem \<open>?'a * ?'b\<close> and
-@{text "?'b list * nat"} from the beginning of this section, and the
+\<open>?'b list * nat\<close> from the beginning of this section, and the
 calculated type environment @{ML tyenv_unif}:
 @{ML_response_fake [display, gray]
 "pretty_tyenv @{context} tyenv_unif"
 "[?'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
+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
-"?'b"} is instantiated to @{typ nat}, this is not propagated to the
+instantiation for \<open>?'a\<close>.  In unification theory, this is often
-instantiation for @{text "?'a"}.  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 *
+performance reasons. To apply such a type environment to a type, say \<open>?'a *
-?'b"}, you should use the function @{ML_ind norm_type in Envir}:
+?'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\"}"
 "nat list * nat"}
 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
-*}
+\<close>
-ML %grayML{*val tyenv_match = let
+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*}
+end\<close>
-text {*
+text \<open>
 Printing out the calculated matcher gives
 @{ML_response_fake [display,gray]
 "pretty_tyenv @{context} tyenv_match"
 "[?'a := bool list, ?'b := nat]"}
 Be careful to observe the difference: always use
 @{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:
-*}
+\<close>
-ML %grayML{*val tyenv_match' = let
+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*}
+end\<close>
-text {*
+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\"}"
 "nat list * nat"}
 as results. These are implemented in @{ML_file "Pure/envir.ML"}.
 This file also includes the substitution and normalisation functions,
 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}
-*}
+\<close>
-text {*
+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"}:
+the function \<open>pretty_env\<close>:
-*}
+\<close>
-ML %grayML{*fun pretty_env ctxt env =
+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*}
+end\<close>
-text {*
+text \<open>
-As can be seen from the @{text "get_trms"}-function, a term environment associates
+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"}.
+\<open>?X ?Y\<close>.
-*}
+\<close>
-ML %grayML{*val (_, fo_env) = let
+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 *}
+end\<close>
-text {*
+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
 @{ML_response_fake [display, gray]
 First-order matching is useful for matching against applications and
 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
+matching \<open>\<lambda>x. P x\<close> against the pattern \<open>\<lambda>y. ?X y\<close>. In this
-case, first-order matching produces @{text "[?X := P]"}.
+case, first-order matching produces \<open>[?X := P]\<close>.
 @{ML_response_fake [display, gray]
 "let
 val fo_pat = @{term_pat \"\<lambda>y. (?X::nat\<Rightarrow>bool) y\"}
 val trm = @{term \"\<lambda>x. (P::nat\<Rightarrow>bool) x\"}
 Pattern.first_order_match @{theory} (fo_pat, trm) init
 |> snd
 |> pretty_env @{context}
 end"
 "[?X := P]"}
-*}
+\<close>
-text {*
+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
 every schematic variable are distinct bounds.
 In particular this excludes terms where a
 pretty_env @{context} (Envir.term_env env)
 end"
 "[?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
+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
-0}) 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
-*}
+\<close>
-ML %grayML{*val uni_seq =
+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 *}
+end\<close>
-text {*
+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"}.
+unifiers \<open>un1\<dots>un3\<close>.
-*}
+\<close>
-ML %grayML{*val SOME ((un1, _), next1) = Seq.pull uni_seq;
+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 *}
+val NONE = Seq.pull next3\<close>
-text {*
+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.
 @{ML_response_fake [display, gray]
 Here we only have a look at a simple case, namely the theorem
 @{thm [source] spec}:
 \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
+this problem is to instantiate the schematic variables \<open>?P\<close> and
-@{text "?x"}.  Instantiation function for theorems is
+\<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}
 This means we have to transform the environment the higher-order matching
 function returns into such an instantiation. For this we use the functions
 @{ML_ind term_env in Envir} and @{ML_ind type_env in Envir}, which extract
 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
-*}
+\<close>
-ML %grayML{*fun prep_trm ctxt (x, (T, t)) =
+ML %grayML\<open>fun prep_trm ctxt (x, (T, t)) =
-((x, T), Thm.cterm_of ctxt t)*}
+((x, T), Thm.cterm_of ctxt t)\<close>
-text {*
+text \<open>
 and into proper @{ML_type cterm}-pairs with
-*}
+\<close>
-ML %grayML{*fun prep_ty ctxt (x, (S, ty)) =
+ML %grayML\<open>fun prep_ty ctxt (x, (S, ty)) =
-((x, S), Thm.ctyp_of ctxt ty)*}
+((x, S), Thm.ctyp_of ctxt ty)\<close>
-text {*
+text \<open>
 We can now calculate the instantiations from the matching function.
-*}
+\<close>
-ML %linenosgray{*fun matcher_inst ctxt pat trm i =
+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
 val tenv = Vartab.dest (Envir.term_env env)
 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
 @{thm [source] spec} rule so that its conclusion is of the form
 @{term "Q True"}.
 in
 Drule.instantiate_normalize inst @{thm spec}
 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}
 Unification and matching of higher-order patterns is implemented in
 @{ML_file "Pure/pattern.ML"}. This file also contains a first-order matcher
 for terms. Full higher-order unification is implemented
 in @{ML_file "Pure/unify.ML"}. It uses lazy sequences which are implemented
 in @{ML_file "Pure/General/seq.ML"}.
 \end{readmore}
-*}
+\<close>
-section {* Sorts (TBD)\label{sec:sorts} *}
+section \<open>Sorts (TBD)\label{sec:sorts}\<close>
-text {*
+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.
 The type-in-class judgement is defined
 via a simple logic over types, with inferences solely based on
 inhabited by all types and is called the topsort.
 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.
-*}
+\<close>
-ML {* Sign.classes_of @{theory} *}
+ML \<open>Sign.classes_of @{theory}\<close>
-ML {* Sign.of_sort @{theory} *}
+ML \<open>Sign.of_sort @{theory}\<close>
-text {*
+text \<open>
 \begin{readmore}
 Classes, sorts and arities are defined in @{ML_file "Pure/term.ML"}.
 @{ML_file "Pure/sorts.ML"} contains comparison and normalization functionality for sorts,
 manages the order sorted algebra and offers an interface for reinterpreting
 (especially names, constants, paths, type classes) a
 theory acquires by theory extension mechanisms and manages associated certification
 functionality.
 It also provides the most needed functionality from individual underlying modules.
 \end{readmore}
-*}
+\<close>
-section {* Type-Checking\label{sec:typechecking} *}
+section \<open>Type-Checking\label{sec:typechecking}\<close>
-text {*
+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.
 Given a well-typed term, the function @{ML_ind type_of in Term} returns the
 type of a term. Consider for example:
 Syntax.check_term @{context} (c $ o $ v)
 end"
 "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
+Instead of giving explicitly the type for the constant \<open>plus\<close> and the free
-variable @{text "x"}, type-inference fills in the missing information.
+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,
 checking and pretty-printing of terms are defined. Functions related to
 type-inference are implemented in @{ML_file "Pure/type.ML"} and
 Check that the function defined in Exercise~\ref{fun:revsum} returns a
 result that type-checks. See what happens to the  solutions of this
 exercise given in Appendix \ref{ch:solutions} when they receive an
 ill-typed term as input.
 \end{exercise}
-*}
+\<close>
-section {* Certified Terms and Certified Types *}
+section \<open>Certified Terms and Certified Types\<close>
-text {*
+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
 a theory.  Type-checking is done via the function @{ML_ind cterm_of in Thm}, which
 converts a @{ML_type term} into a @{ML_type cterm}, a \emph{certified}
 \begin{readmore}
 For functions related to @{ML_type cterm}s and @{ML_type ctyp}s see
 the files @{ML_file "Pure/thm.ML"}, @{ML_file "Pure/more_thm.ML"} and
 @{ML_file "Pure/drule.ML"}.
 \end{readmore}
-*}
+\<close>
-section {* Theorems\label{sec:theorems} *}
+section \<open>Theorems\label{sec:theorems}\<close>
-text {*
+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.
 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:
-*}
+\<close>
-ML %linenosgray{*val my_thm =
+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"}
 val Pt_implies_Qt =
 val Qt = Thm.implies_elim Pt_implies_Qt (Thm.assume assm2)
 in
 Qt
 |> Thm.implies_intr assm2
 |> Thm.implies_intr assm1
-end*}
+end\<close>
-text {*
+text \<open>
-Note that in Line 3 and 4 we use the antiquotation @{text "@{cprop \<dots>}"}, which
+Note that in Line 3 and 4 we use the antiquotation \<open>@{cprop \<dots>}\<close>, which
-inserts necessary @{text "Trueprop"}s.
+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.
 @{ML_response_fake [display, gray]
 However, internally the code-snippet constructs the following
 proof.
 \[
-\infer[(@{text "\<Longrightarrow>"}$-$intro)]{\vdash @{prop "(\<And>x. P x \<Longrightarrow> Q x) \<Longrightarrow> 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[(@{text "\<Longrightarrow>"}$-$intro)]{@{prop "\<And>x. P x \<Longrightarrow> Q x"} \vdash @{prop "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[(@{text "\<Longrightarrow>"}$-$elim)]{@{prop "\<And>x. P x \<Longrightarrow> Q x"}, @{prop "P t"} \vdash @{prop "Q t"}}
+{\infer[(\<open>\<Longrightarrow>\<close>$-$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>\<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"}}{}
 }
 }
 referenced on the user level. One way to store it in the theorem database is
 by using the function @{ML_ind note in Local_Theory} from the structure
 @{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*}
+end\<close>
-local_setup %gray {*
+local_setup %gray \<open>
-Local_Theory.note ((@{binding "my_thm"}, []), [my_thm_vars]) #> snd *}
+Local_Theory.note ((@{binding "my_thm"}, []), [my_thm_vars]) #> snd\<close>
-text {*
+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
 which we store the theorem or theorems. The second argument can contain a
 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:
-*}
+\<close>
-local_setup %gray {*
+local_setup %gray \<open>
 Local_Theory.note ((@{binding "my_thm_simp"},
-[Attrib.internal (K Simplifier.simp_add)]), [my_thm_vars]) #> snd *}
+[Attrib.internal (K Simplifier.simp_add)]), [my_thm_vars]) #> snd\<close>
-text {*
+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
 internal in Attrib} from the structure @{ML_struct Attrib}. If we use the function
 @{ML get_thm_names_from_ss} from
 [source] my_thm_simp} is that they can now also be referenced with the
 \isacommand{thm}-command on the user-level of Isabelle
 \begin{isabelle}
-\isacommand{thm}~@{text "my_thm my_thm_simp"}\isanewline
+\isacommand{thm}~\<open>my_thm my_thm_simp\<close>\isanewline
-@{text ">"}~@{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"}\isanewline
-@{text ">"}~@{prop "\<lbrakk>\<And>x. P x \<Longrightarrow> Q x; P t\<rbrakk> \<Longrightarrow> Q t"}
+\<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
 with the same theorem name. In effect, once a theorem is stored under a name,
 this association is fixed. While this is a ``safety-net'' to make sure a
 theorem name refers to a particular theorem or collection of theorems, it is
 also a bit too restrictive in cases where a theorem name should refer to a
 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}.
+To see how it works let us assume we defined our own theorem list \<open>MyThmList\<close>.
-*}
+\<close>
-ML %grayML{*structure MyThmList = Generic_Data
+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))*}
+fun update thm = Context.theory_map (MyThmList.map (Thm.add_thm thm))\<close>
-text {*
+text \<open>
 The function @{ML update} allows us to update the theorem list, for example
 by adding the theorem @{thm [source] TrueI}.
-*}
+\<close>
-setup %gray {* update @{thm TrueI} *}
+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}
-*}
+\<close>
-setup %gray {*
+setup %gray \<open>
 Global_Theory.add_thms_dynamic (@{binding "mythmlist"}, MyThmList.get)
-*}
+\<close>
-text {*
+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"}\\
+\isacommand{thm}~\<open>mythmlist\<close>\\
-@{text "> True"}
+\<open>> True\<close>
 \end{isabelle}
 the current content of the theorem list is displayed. If more theorems are stored in
 the list, say
-*}
+\<close>
-setup %gray {* update @{thm FalseE} *}
+setup %gray \<open>update @{thm FalseE}\<close>
-text {*
+text \<open>
 then the same command produces
 \begin{isabelle}
-\isacommand{thm}~@{text "mythmlist"}\\
+\isacommand{thm}~\<open>mythmlist\<close>\\
-@{text "> False \<Longrightarrow> ?P"}\\
+\<open>> False \<Longrightarrow> ?P\<close>\\
-@{text "> True"}
+\<open>> True\<close>
 \end{isabelle}
 Note that if we add the theorem @{thm [source] FalseE} again to the list
-*}
+\<close>
-setup %gray {* update @{thm FalseE} *}
+setup %gray \<open>update @{thm FalseE}\<close>
-text {*
+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]
 "(Thm.eq_thm_prop (@{thm thm1}, @{thm thm2}),
 Thm.eq_thm_prop (@{thm thm2}, @{thm thm3}))"
 end"
 "(True, (\<lambda>x. x) = (\<lambda>x. x))"}
 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]
 "let
 val ctxt = @{context}
 "Premises: ?A, ?B
 Conclusion: ?C
 Premises:
 Conclusion: ?A \<longrightarrow> ?B \<longrightarrow> ?C"}
-Note that in the second case, there is no premise. The reason is that @{text "\<Longrightarrow>"}
+Note that in the second case, there is no premise. The reason is that \<open>\<Longrightarrow>\<close>
-separates premises and conclusion, while @{text "\<longrightarrow>"} is the object implication
+separates premises and conclusion, while \<open>\<longrightarrow>\<close> is the object implication
 from HOL, which just constructs a formula.
 \begin{readmore}
 The basic functions for theorems are defined in
 @{ML_file "Pure/thm.ML"}, @{ML_file "Pure/more_thm.ML"} and @{ML_file "Pure/drule.ML"}.
 |> pretty_thm @{context}
 |> pwriteln"
 "(\<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>"}
+logic, that is replacing all \<open>\<longrightarrow>\<close> and \<open>\<forall>\<close> by \<open>\<Longrightarrow>\<close>
-and @{text "\<And>"}, or the other way around.  A reason for such a transformation
+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
 some build in functions which help with these transformations. The function
 @{ML_ind rulify in Object_Logic}
 involving meta variables, such as @{thm [source] list.induct}, which
 is of the form
 @{thm [display] list.induct}
-we have to first abstract over the meta variables @{text "?P"} and
+we have to first abstract over the meta variables \<open>?P\<close> and
-@{text "?list"}. For this we can use the function
+\<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.
-*}
+\<close>
-ML %grayML{*fun atomize_thm ctxt thm =
+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*}
+end\<close>
-text {*
+text \<open>
 This function produces for the theorem @{thm [source] list.induct}
 @{ML_response_fake [display, gray]
 "atomize_thm @{context} @{thm list.induct}"
 "\<forall>P list. P [] \<longrightarrow> (\<forall>a list. P list \<longrightarrow> P (a # list)) \<longrightarrow> P list"}
 end"
 "?P \<Longrightarrow> ?P"}
 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.
 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.
-*}
+\<close>
-ML %grayML{*fun rep_goals i = replicate i @{prop "f x = f x"}
+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))*}
+(K ((Goal.conjunction_tac THEN' RANGE (rep_tacs i)) 1))\<close>
-text {*
+text \<open>
 With them we can now produce three theorem instances of the
 proposition.
 @{ML_response_fake [display, gray]
 "multi_test @{context} 3"
 "[\"?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*}
+end\<close>
-text {*
+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.
 Potentially making the system unsound.  This is sometimes useful for developing
 purposes, or when explicit proof construction should be omitted due to performace
 Theorems also contain auxiliary data, such as the name of the theorem, its
 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
 @{ML_response_fake [display,gray]
 "Thm.get_tags @{thm foo_data}"
 consisting of a name and a kind.  When we store lemmas in the theorem database,
 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}.
-*}
+\<close>
-local_setup %gray {*
+local_setup %gray \<open>
 Local_Theory.note ((@{binding "foo_data'"}, []),
 [(Rule_Cases.name ["foo_case_one", "foo_case_two"]
-@{thm foo_data})]) #> snd *}
+@{thm foo_data})]) #> snd\<close>
-text {*
+text \<open>
 The data of the theorem @{thm [source] foo_data'} is then as follows:
 @{ML_response_fake [display,gray]
 "Thm.get_tags @{thm foo_data'}"
 "[(\"name\", \"General.foo_data'\"), (\"kind\", \"lemma\"),
 (\"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:"}\\
+\<open>> cases:\<close>\\
-@{text ">   foo_case_one:"}\\
+\<open>>   foo_case_one:\<close>\\
-@{text ">     let \"?case\" = \"?P\""}\\
+\<open>>     let "?case" = "?P"\<close>\\
-@{text ">   foo_case_two:"}\\
+\<open>>   foo_case_two:\<close>\\
-@{text ">     let \"?case\" = \"?P\""}
+\<open>>     let "?case" = "?P"\<close>
-\end{tabular}*}
+\end{tabular}\<close>
-text {*
+text \<open>
-we can proceed by analysing the cases @{text "foo_case_one"} and
+we can proceed by analysing the cases \<open>foo_case_one\<close> and
-@{text "foo_case_two"}. While if the theorem has no names, then
+\<open>foo_case_two\<close>. While if the theorem has no names, then
-the cases have standard names @{text 1}, @{text 2} and so
+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:"}\\
+\<open>> cases:\<close>\\
-@{text ">   1:"}\\
+\<open>>   1:\<close>\\
-@{text ">     let \"?case\" = \"?P\""}\\
+\<open>>     let "?case" = "?P"\<close>\\
-@{text ">   2:"}\\
+\<open>>   2:\<close>\\
-@{text ">     let \"?case\" = \"?P\""}
+\<open>>     let "?case" = "?P"\<close>
-\end{tabular}*}
+\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
+proving a theorem, especially when the proof is by \<open>auto\<close>. These theorems can be obtained by introspecting the proved theorem.
-auto}. 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}.
-*}
+\<close>
-ML %grayML{*fun pthms_of (PBody {thms, ...}) = map #2 thms
+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 *}
+val get_pbodies = map (Future.join o Proofterm.thm_node_body) o pthms_of\<close>
-text {*
+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"
 apply(rule conjI)
 apply(drule conjunct1)
 shows "A \<and> B \<Longrightarrow> A \<and> B"
 apply(auto)
 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
 established theorem. This can be done with
 "@{thm my_conjIa}
 |> Thm.proof_body_of
 |> 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
 three theorems, namely @{thm [source] conjI}, @{thm [source] conjunct1}
 and @{thm [source] conjunct2}. We can obtain them by descending into the
 "[\"HOL.conjunct2\", \"HOL.conjunct1\", \"HOL.conjI\", \"Pure.protectD\",
 \"Pure.protectI\"]"}
 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]
 "@{thm my_conjIb}
 |> Thm.proof_body_of
 sometimes the verbatim quoting is not what is wanted or what can be shown to
 readers. For such situations Isabelle allows the installation of \emph{\index*{theorem
 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
+leading \<open>\<forall>\<close>-quantifiers. For this we can implement the following function
-that strips off @{text "\<forall>"}s.
+that strips off \<open>\<forall>\<close>s.
-*}
+\<close>
-ML %linenosgray{*fun strip_allq (Const (@{const_name "All"}, _) $ Abs body) =
+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*}
+| strip_allq t = t\<close>
-text {*
+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"}.
+install this function as the theorem style named \<open>my_strip_allq\<close>.
-*}
+\<close>
-setup %gray{*
+setup %gray\<open>
 Term_Style.setup @{binding "my_strip_allq"} (Scan.succeed (K strip_allq))
-*}
+\<close>
-text {*
+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}"}\\
+\<open>@{thm style_test}\<close>\\
-@{text ">"}~@{thm style_test}
+\<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}"}\\
+\<open>@{thm (my_strip_allq) style_test}\<close>\\
-@{text ">"}~@{thm (my_strip_allq) style_test}
+\<open>>\<close>~@{thm (my_strip_allq) style_test}
 \end{graybox}
 \end{isabelle}
 without the leading quantifiers. We can improve this theorem style by explicitly
 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.
-*}
+\<close>
-ML %grayML{*fun rename_allq [] t = t
+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*}
+| rename_allq _ t = t\<close>
-text {*
+text \<open>
 We can now install a the modified theorem style as follows
-*}
+\<close>
-setup %gray {* let
+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 *}
+end\<close>
-text {*
+text \<open>
-The parser reads a list of names. In the function @{text action} we first
+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}"}\\
+\<open>@{thm (my_strip_allq2 x' x'') style_test}\<close>\\
-@{text ">"}~@{thm (my_strip_allq2 x' x'') style_test}
+\<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 ...}"}
+antiquotations \<open>@{prop ...}\<close>, \<open>@{term_type ...}\<close>
-and @{text "@{typeof ...}"}.
+and \<open>@{typeof ...}\<close>.
 Next we explain theorem attributes, which is another
 mechanism for dealing with theorems.
 \begin{readmore}
 Theorem styles are implemented in @{ML_file "Pure/Thy/term_style.ML"}.
 \end{readmore}
-*}
+\<close>
-section {* Theorem Attributes\label{sec:attributes} *}
+section \<open>Theorem Attributes\label{sec:attributes}\<close>
-text {*
+text \<open>
-Theorem attributes are @{text "[symmetric]"}, @{text "[THEN \<dots>]"}, @{text
+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
-"[simp]"} 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
 the function behind the attribute stores the theorems in a retrievable
 data structure.
 If you want to print out all currently known attributes a theorem can have,
 you can use the Isabelle command
 \begin{isabelle}
 \isacommand{print\_attributes}\\
-@{text "> COMP:  direct composition with rules (no lifting)"}\\
+\<open>> COMP:  direct composition with rules (no lifting)\<close>\\
-@{text "> HOL.dest:  declaration of Classical destruction rule"}\\
+\<open>> HOL.dest:  declaration of Classical destruction rule\<close>\\
-@{text "> HOL.elim:  declaration of Classical elimination rule"}\\
+\<open>> HOL.elim:  declaration of Classical elimination rule\<close>\\
-@{text "> \<dots>"}
+\<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
+theorems (for example \<open>[symmetric]\<close> and \<open>[THEN \<dots>]\<close>), and the second
-stores theorems somewhere as data (for example @{text "[simp]"}, which adds
+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
-*}
+\<close>
-ML %grayML{*val my_symmetric = Thm.rule_attribute [] (fn _ => fn thm => thm RS @{thm sym})*}
+ML %grayML\<open>val my_symmetric = Thm.rule_attribute [] (fn _ => fn thm => thm RS @{thm sym})\<close>
-text {*
+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
+context (which we ignore in the code above) and a theorem (\<open>thm\<close>), and
-returns another theorem (namely @{text thm} resolved with the theorem
+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"
+\<open>Scan.succeed my_symmetric\<close> "applying the sym rule"
-text {*
+text \<open>
-Inside the @{text "\<verbopen> \<dots> \<verbclose>"}, we have to specify a parser
+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
+arguments (unlike \<open>[THEN \<dots>]\<close>, for instance), we use the parser @{ML
-Scan.succeed}. An example for the attribute @{text "[my_sym]"} is the proof
+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"}\\
+\isacommand{thm}~\<open>test\<close>\\
-@{text "> "}~@{thm test}
+\<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]"}\\
+\isacommand{thm}~\<open>test[my_sym]\<close>\\
-@{text "> "}~@{thm test[my_sym]}
+\<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:
-*}
+\<close>
-ML %grayML{*Attrib.setup @{binding "my_sym"} (Scan.succeed my_symmetric)
+ML %grayML\<open>Attrib.setup @{binding "my_sym"} (Scan.succeed my_symmetric)
-"applying the sym rule" *}
+"applying the sym rule"\<close>
-text {*
+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
-*}
+\<close>
-ML %grayML{*fun MY_THEN thms =
+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*}
+end\<close>
-text {*
+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.
-*}
+\<close>
-attribute_setup %gray MY_THEN = {* Attrib.thms >> MY_THEN *}
+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]"}\\
+\isacommand{thm}~\<open>test[MY_THEN eq_reflection]\<close>\\
-@{text "> "}~@{thm test[MY_THEN eq_reflection]}
+\<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]"}\\
+\isacommand{thm}~\<open>test[MY_THEN sym eq_reflection]\<close>\\
-@{text "> "}~@{thm test[MY_THEN sym eq_reflection]}
+\<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]"}\\
+\isacommand{thm}~\<open>test[my_sym, MY_THEN eq_reflection]\<close>\\
-@{text "> "}~@{thm test[my_sym, MY_THEN eq_reflection]}
+\<open>> \<close>~@{thm test[my_sym, MY_THEN eq_reflection]}
 \end{isabelle}
 However, here also a weakness of the concept
 of theorem attributes shows through: since theorem attributes can be
 arbitrary functions, they do not commute in general. If you try
 \begin{isabelle}
-\isacommand{thm}~@{text "test[MY_THEN eq_reflection, my_sym]"}\\
+\isacommand{thm}~\<open>test[MY_THEN eq_reflection, my_sym]\<close>\\
-@{text "> "}~@{text "exception THM 1 raised: RSN: no unifiers"}
+\<open>> \<close>~\<open>exception THM 1 raised: RSN: no unifiers\<close>
 \end{isabelle}
 you get an exception indicating that the theorem @{thm [source] sym}
 does not resolve with meta-equations.
 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.
-*}
+\<close>
-ML %grayML{*structure MyThms = Named_Thms
+ML %grayML\<open>structure MyThms = Named_Thms
 (val name = @{binding "attr_thms"}
-val description = "Theorems for an Attribute") *}
+val description = "Theorems for an Attribute")\<close>
-text {*
+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
-*}
+\<close>
-ML %grayML{*val my_add = Thm.declaration_attribute MyThms.add_thm
+ML %grayML\<open>val my_add = Thm.declaration_attribute MyThms.add_thm
-val my_del = Thm.declaration_attribute MyThms.del_thm *}
+val my_del = Thm.declaration_attribute MyThms.del_thm\<close>
-text {*
+text \<open>
 and set up the attributes as follows
-*}
+\<close>
-attribute_setup %gray my_thms = {* Attrib.add_del my_add my_del *}
+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]
 "MyThms.get @{context}"
 "[\"True\"]"}
 You can also add theorems using the command \isacommand{declare}.
-*}
+\<close>
 declare test[my_thms] trueI_2[my_thms add]
-text {*
+text \<open>
-With this attribute, the @{text "add"} operation is the default and does
+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:
 @{ML_response_fake [display,gray]
 "MyThms.get @{context}"
 "[\"True\", \"Suc (Suc 0) = 2\"]"}
 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}"
 "[\"True\"]"}
 We used in this example two functions declared as @{ML_ind
 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}
 FIXME: @{ML_file "Pure/more_thm.ML"}; parsers for attributes is in
 @{ML_file "Pure/Isar/attrib.ML"}...also explained in the chapter about
 parsing.
 \end{readmore}
-*}
+\<close>
-section {* Pretty-Printing\label{sec:pretty} *}
+section \<open>Pretty-Printing\label{sec:pretty}\<close>
-text {*
+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
 sophisticated, Isabelle includes an infrastructure for properly formatting
 text. Most of its functions do not operate on @{ML_type string}s, but on
 text should be printed.  However, if you want to actually output the
 formatted text, you have to transform the pretty type back into a @{ML_type
 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:
-*}
+\<close>
-ML %grayML{*fun pprint prt = tracing (Pretty.string_of prt)*}
+ML %grayML\<open>fun pprint prt = tracing (Pretty.string_of prt)\<close>
-text {*
+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:
-*}
+\<close>
-ML %grayML{*fun rep n str = implode (replicate n str) *}
+ML %grayML\<open>fun rep n str = implode (replicate n str)\<close>
-text {*
+text \<open>
 and suppose we want to print out the string:
-*}
+\<close>
-ML %grayML{*val test_str = rep 8 "fooooooooooooooobaaaaaaaaaaaar "*}
+ML %grayML\<open>val test_str = rep 8 "fooooooooooooooobaaaaaaaaaaaar "\<close>
-text {*
+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:
 @{ML_response_fake [display,gray]
 where @{ML upto} generates a list of integers. You can print out this
 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
-*}
+\<close>
-text {*
+text \<open>
 @{ML_response_fake [display,gray]
 "let
 val ptrs = map (Pretty.str o string_of_int) (99998 upto 100020)
 in
 standard functions, you can do relatively easily the formatting
 yourself. Assume you want to print out a list of items where like in ``English''
 the last two items are separated by @{text [quotes] "and"}. For this you can
 write the function
-*}
+\<close>
-ML %linenosgray{*fun and_list [] = []
+ML %linenosgray\<open>fun and_list [] = []
 | and_list [x] = [x]
 | and_list xs =
 let
 val (front, last) = split_last xs
 in
 (Pretty.commas front) @
 [Pretty.brk 1, Pretty.str "and", Pretty.brk 1, last]
-end *}
+end\<close>
-text {*
+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
 @{text [quotes] "and"}. This space is also a place where a line break
 can occur. We do the same after the @{text [quotes] "and"}. This gives you
 (P 1 = P 4 \<longrightarrow> P 4 \<and> P 3 \<and> P 2 \<and> P 1) \<longrightarrow>
 P 4 \<and> P 3 \<and> P 2 \<and> P 1"}
 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"}.
+function \<open>tell_type\<close>.
-*}
+\<close>
-ML %linenosgray{*fun tell_type ctxt trm =
+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)
 val pty  = Pretty.quote (Syntax.pretty_typ ctxt (fastype_of trm))
 in
 pprint (Pretty.blk (0,
 (pstr "The term " @ [ptrm] @ pstr " has type "
 @ [pty, Pretty.str "."])))
-end*}
+end\<close>
-text {*
+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
 pretty_typ in Syntax}. We also use the function @{ML_ind quote in
 Pretty} in order to enclose the term and type inside quotation marks. In
 @{ML_file "Pure/General/pretty.ML"}. The file @{ML_file "Pure/Syntax/syntax.ML"}
 contains pretty-printing functions for terms, types, theorems and so on.
 @{ML_file "Pure/PIDE/markup.ML"}
 \end{readmore}
-*}
+\<close>
-section {* Summary *}
+section \<open>Summary\<close>
-text {*
+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

changeset 565	cecd7a941885
parent 562	daf404920ab9
child 566	6103b0eadbf2