# HG changeset patch
# User Norbert Schirmer <norbert.schirmer@web.de>
# Date 1558082281 -7200
# Node ID f875a25aa72d854e9e33787429802230d007b742
# Parent  be23597e81dbf47b006f6e9a3217fec190a09067
prefer cartouches over " in ML antiquotations

diff -r be23597e81db -r f875a25aa72d ProgTutorial/Advanced.thy
--- a/ProgTutorial/Advanced.thy	Fri May 17 07:29:51 2019 +0200
+++ b/ProgTutorial/Advanced.thy	Fri May 17 10:38:01 2019 +0200
@@ -132,14 +132,13 @@
 
   \begin{isabelle}
   \begin{graybox}
-  \isacommand{setup}~\<open>\<verbopen>\<close> @{ML
-"fn thy => 
+  \isacommand{setup}~\<open>\<verbopen>\<close> @{ML \<open>fn thy => 
 let
-  val bar_const = ((@{binding \"BAR\"}, @{typ \"nat\"}), NoSyn)
+  val bar_const = ((@{binding "BAR"}, @{typ "nat"}), NoSyn)
   val (_, thy') = Sign.declare_const @{context} bar_const thy
 in
   thy
-end"}~\<open>\<verbclose>\<close>\isanewline
+end\<close>}~\<open>\<verbclose>\<close>\isanewline
   \<open>> ERROR: "Stale theory encountered"\<close>
   \end{graybox}
   \end{isabelle}
@@ -215,14 +214,14 @@
 
   \begin{isabelle}
   \begin{graybox}
-  @{ML "let
-  val trm = @{term \"(x, y, z, w)\"}
+  @{ML \<open>let
+  val trm = @{term "(x, y, z, w)"}
 in
   pwriteln (Pretty.chunks 
     [ pretty_term ctxt0 trm,
       pretty_term ctxt1 trm,
       pretty_term ctxt2 trm ])
-end"}\\
+end\<close>}\\
   \setlength{\fboxsep}{0mm}
   \<open>>\<close>~\<open>(\<close>\colorbox{gray!5}{\raisebox{0mm}[3mm][1mm]{\<open>x\<close>}}\<open>,\<close>~%
   \colorbox{gray!5}{\raisebox{0mm}[3mm][1mm]{\<open>y\<close>}}\<open>,\<close>~%
@@ -241,9 +240,8 @@
 
 
   The term we are printing is in all three cases the same---a tuple containing
-  four free variables. As you can see, however, in case of @{ML "ctxt0"} all
-  variables are highlighted indicating a problem, while in case of @{ML
-  "ctxt1"} \<open>x\<close> and \<open>y\<close> are printed as normal (blue) free
+  four free variables. As you can see, however, in case of @{ML \<open>ctxt0\<close>} all
+  variables are highlighted indicating a problem, while in case of @{ML \<open>ctxt1\<close>} \<open>x\<close> and \<open>y\<close> are printed as normal (blue) free
   variables, but not \<open>z\<close> and \<open>w\<close>. In the last case all variables
   are printed as expected. The point of this example is that the context
   contains the information which variables are fixed, and designates all other
@@ -253,18 +251,18 @@
   fixing a variable twice
 
   @{ML_matchresult_fake [gray, display]
-  "@{context}
-|> Variable.add_fixes [\"x\", \"x\"]" 
-  "ERROR: Duplicate fixed variable(s): \"x\""}
+  \<open>@{context}
+|> Variable.add_fixes ["x", "x"]\<close> 
+  \<open>ERROR: Duplicate fixed variable(s): "x"\<close>}
 
   More importantly it also allows us to easily create fresh names for
   fixed variables.  For this you have to use the function @{ML_ind
   variant_fixes in Variable} from the structure @{ML_structure Variable}.
 
   @{ML_matchresult_fake [gray, display]
-  "@{context}
-|> Variable.variant_fixes [\"y\", \"y\", \"z\"]" 
-  "([\"y\", \"ya\", \"z\"], ...)"}
+  \<open>@{context}
+|> Variable.variant_fixes ["y", "y", "z"]\<close> 
+  \<open>(["y", "ya", "z"], ...)\<close>}
 
   Now a fresh variant for the second occurence of \<open>y\<close> is created
   avoiding any clash. In this way we can also create fresh free variables
@@ -274,16 +272,16 @@
   string @{text [quotes] "x"} (Lines 6 and 7).
 
   @{ML_matchresult_fake [display, gray, linenos]
-  "let
+  \<open>let
   val ctxt0 = @{context}
-  val (_, ctxt1) = Variable.add_fixes [\"x\"] ctxt0
-  val frees = replicate 2 (\"x\", @{typ nat})
+  val (_, ctxt1) = Variable.add_fixes ["x"] ctxt0
+  val frees = replicate 2 ("x", @{typ nat})
 in
   (Variable.variant_frees ctxt0 [] frees,
    Variable.variant_frees ctxt1 [] frees)
-end"
-  "([(\"x\", \"nat\"), (\"xa\", \"nat\")], 
- [(\"xa\", \"nat\"), (\"xb\", \"nat\")])"}
+end\<close>
+  \<open>([("x", "nat"), ("xa", "nat")], 
+ [("xa", "nat"), ("xb", "nat")])\<close>}
 
   As you can see, if we create the fresh variables with the context \<open>ctxt0\<close>,
   then we obtain \<open>x\<close> and \<open>xa\<close>; but in \<open>ctxt1\<close> we obtain \<open>xa\<close>
@@ -294,13 +292,13 @@
   function @{ML_ind declare_term in Variable} from the structure @{ML_structure Variable}.
 
   @{ML_matchresult_fake [gray, display]
-  "let
-  val ctxt1 = Variable.declare_term @{term \"(x, xa)\"} @{context}
-  val frees = replicate 2 (\"x\", @{typ nat})
+  \<open>let
+  val ctxt1 = Variable.declare_term @{term "(x, xa)"} @{context}
+  val frees = replicate 2 ("x", @{typ nat})
 in
   Variable.variant_frees ctxt1 [] frees
-end"
-  "[(\"xb\", \"nat\"), (\"xc\", \"nat\")]"}
+end\<close>
+  \<open>[("xb", "nat"), ("xc", "nat")]\<close>}
 
   The result is \<open>xb\<close> and \<open>xc\<close> for the names of the fresh
   variables, since \<open>x\<close> and \<open>xa\<close> occur in the term we declared. 
@@ -310,12 +308,12 @@
 
   \begin{isabelle}
   \begin{graybox}
-  @{ML "let
-  val trm = @{term \"P x y z\"}
+  @{ML \<open>let
+  val trm = @{term "P x y z"}
   val ctxt1 = Variable.declare_term trm @{context}
 in
   pwriteln (pretty_term ctxt1 trm)
-end"}\\
+end\<close>}\\
   \setlength{\fboxsep}{0mm}
   \<open>>\<close>~\colorbox{gray!5}{\raisebox{0mm}[3mm][1mm]{\<open>P\<close>}}~%
   \colorbox{gray!5}{\raisebox{0mm}[3mm][1mm]{\<open>x\<close>}}~%
@@ -330,14 +328,14 @@
   @{ML_structure Syntax}. Consider the following code:
 
   @{ML_matchresult_fake [gray, display]
-  "let
+  \<open>let
   val ctxt0 = @{context}
-  val ctxt1 = Variable.declare_term @{term \"x::nat\"} ctxt0
+  val ctxt1 = Variable.declare_term @{term "x::nat"} ctxt0
 in
-  (Syntax.read_term ctxt0 \"x\", 
-   Syntax.read_term ctxt1 \"x\") 
-end"
-  "(Free (\"x\", \"'a\"), Free (\"x\", \"nat\"))"}
+  (Syntax.read_term ctxt0 "x", 
+   Syntax.read_term ctxt1 "x") 
+end\<close>
+  \<open>(Free ("x", "'a"), Free ("x", "nat"))\<close>}
   
   Parsing the string in the context \<open>ctxt0\<close> results in a free variable 
   with a default polymorphic type, but in case of \<open>ctxt1\<close> we obtain a
@@ -346,14 +344,14 @@
   is made, as the next example illustrates.
 
   @{ML_matchresult_fake [gray, display]
-  "let
-  val ctxt1 = Variable.declare_term @{term \"x::nat\"} @{context}
-  val ctxt2 = Variable.declare_term @{term \"x::int\"} ctxt1
+  \<open>let
+  val ctxt1 = Variable.declare_term @{term "x::nat"} @{context}
+  val ctxt2 = Variable.declare_term @{term "x::int"} ctxt1
 in
-  (Syntax.read_term ctxt1 \"x\", 
-   Syntax.read_term ctxt2 \"x\") 
-end"
-  "(Free (\"x\", \"nat\"), Free (\"x\", \"int\"))"}
+  (Syntax.read_term ctxt1 "x", 
+   Syntax.read_term ctxt2 "x") 
+end\<close>
+  \<open>(Free ("x", "nat"), Free ("x", "int"))\<close>}
 
   The most useful feature of contexts is that one can export, or transfer, 
   terms and theorems between them. We show this first for terms. 
@@ -361,15 +359,15 @@
   \begin{isabelle}
   \begin{graybox}
   \begin{linenos}
-  @{ML "let
+  @{ML \<open>let
   val ctxt0 = @{context}
-  val (_, ctxt1) = Variable.add_fixes [\"x\", \"y\", \"z\"] ctxt0 
-  val foo_trm = @{term \"P x y z\"}
+  val (_, ctxt1) = Variable.add_fixes ["x", "y", "z"] ctxt0 
+  val foo_trm = @{term "P x y z"}
 in
   singleton (Variable.export_terms ctxt1 ctxt0) foo_trm
   |> pretty_term ctxt0
   |> pwriteln
-end"}
+end\<close>}
   \end{linenos}
   \setlength{\fboxsep}{0mm}
   \<open>>\<close>~\colorbox{gray!5}{\raisebox{0mm}[3mm][1mm]{\<open>P\<close>}}~%
@@ -401,15 +399,15 @@
   whether it is actually provable).
 
   @{ML_matchresult_fake [display, gray]
-  "let
+  \<open>let
   val thy = @{theory}
   val ctxt0 = @{context}
-  val (_, ctxt1) = Variable.add_fixes [\"P\", \"x\", \"y\", \"z\"] ctxt0 
-  val foo_thm = Skip_Proof.make_thm thy @{prop \"P x y z x y z\"}
+  val (_, ctxt1) = Variable.add_fixes ["P", "x", "y", "z"] ctxt0 
+  val foo_thm = Skip_Proof.make_thm thy @{prop "P x y z x y z"}
 in
   singleton (Proof_Context.export ctxt1 ctxt0) foo_thm
-end"
-  "?P ?x ?y ?z ?x ?y ?z"}
+end\<close>
+  \<open>?P ?x ?y ?z ?x ?y ?z\<close>}
 
   Since we fixed all variables in \<open>ctxt1\<close>, in the exported
   result all of them are schematic. The great point of contexts is
@@ -419,14 +417,14 @@
   @{ML_structure Assumption}. Consider the following code.
 
   @{ML_matchresult_fake [display, gray, linenos]
-  "let
+  \<open>let
   val ctxt0 = @{context}
-  val ([eq], ctxt1) = Assumption.add_assumes [@{cprop \"x \<equiv> y\"}] ctxt0
+  val ([eq], ctxt1) = Assumption.add_assumes [@{cprop "x \<equiv> y"}] ctxt0
   val eq' = Thm.symmetric eq
 in
   Assumption.export false ctxt1 ctxt0 eq'
-end"
-  "x \<equiv> y \<Longrightarrow> y \<equiv> x"}
+end\<close>
+  \<open>x \<equiv> y \<Longrightarrow> y \<equiv> x\<close>}
   
   The function @{ML_ind add_assumes in Assumption} from the structure
   @{ML_structure Assumption} adds the assumption \mbox{\<open>x \<equiv> y\<close>}
@@ -451,16 +449,16 @@
   in the following example.
 
   @{ML_matchresult_fake [display, gray]
-  "let
+  \<open>let
   val ctxt0 = @{context}
   val ((fvs, [eq]), ctxt1) = ctxt0
-    |> Variable.add_fixes [\"x\", \"y\"]
-    ||>> Assumption.add_assumes [@{cprop \"x \<equiv> y\"}]
+    |> Variable.add_fixes ["x", "y"]
+    ||>> Assumption.add_assumes [@{cprop "x \<equiv> y"}]
   val eq' = Thm.symmetric eq
 in
   Proof_Context.export ctxt1 ctxt0 [eq']
-end"
-  "[?x \<equiv> ?y \<Longrightarrow> ?y \<equiv> ?x]"}
+end\<close>
+  \<open>[?x \<equiv> ?y \<Longrightarrow> ?y \<equiv> ?x]\<close>}
 \<close>
 
 
@@ -515,7 +513,7 @@
   @{ML_type "Proof.context"}, although not every proof context constitutes a
   valid local theory.
 
-  @{ML "Context.>> o Context.map_theory"}
+  @{ML \<open>Context.>> o Context.map_theory\<close>}
   @{ML_ind "Local_Theory.declaration"}
 
    A similar command is \isacommand{local\_setup}, which expects a function
@@ -590,8 +588,8 @@
   antiquotation \<open>@{binding \<dots>}\<close>. For example
 
   @{ML_matchresult [display,gray]
-  "@{binding \"name\"}"
-  "name"}
+  \<open>@{binding "name"}\<close>
+  \<open>name\<close>}
 
   An example where a qualified name is needed is the function 
   @{ML_ind define in Local_Theory}.  This function is used below to define 
@@ -634,7 +632,7 @@
   Occasionally you have to calculate what the ``base'' name of a given
   constant is. For this you can use the function @{ML_ind  Long_Name.base_name}. For example:
 
-  @{ML_matchresult [display,gray] "Long_Name.base_name \"List.list.Nil\"" "\"Nil\""}
+  @{ML_matchresult [display,gray] \<open>Long_Name.base_name "List.list.Nil"\<close> \<open>"Nil"\<close>}
 
   \begin{readmore}
   Functions about naming are implemented in @{ML_file "Pure/General/name_space.ML"};
diff -r be23597e81db -r f875a25aa72d ProgTutorial/Appendix.thy
--- a/ProgTutorial/Appendix.thy	Fri May 17 07:29:51 2019 +0200
+++ b/ProgTutorial/Appendix.thy	Fri May 17 10:38:01 2019 +0200
@@ -13,7 +13,7 @@
 
   \begin{itemize}
   \item translations/print translations; 
-  @{ML "Proof_Context.print_syntax"}
+  @{ML \<open>Proof_Context.print_syntax\<close>}
   
   \item user space type systems (in the form that already exists)
 
diff -r be23597e81db -r f875a25aa72d ProgTutorial/Essential.thy
--- a/ProgTutorial/Essential.thy	Fri May 17 07:29:51 2019 +0200
+++ b/ProgTutorial/Essential.thy	Fri May 17 10:38:01 2019 +0200
@@ -28,9 +28,9 @@
   using the antiquotation \mbox{\<open>@{term \<dots>}\<close>}. For example
 
   @{ML_matchresult [display,gray] 
-"@{term \"(a::nat) + b = c\"}" 
-"Const (\"HOL.eq\", _) $ 
-  (Const (\"Groups.plus_class.plus\", _) $ _ $ _) $ _"}
+\<open>@{term "(a::nat) + b = c"}\<close> 
+\<open>Const ("HOL.eq", _) $ 
+  (Const ("Groups.plus_class.plus", _) $ _ $ _) $ _\<close>}
 
   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"}, 
@@ -54,8 +54,8 @@
   variables.  For example in
 
   @{ML_matchresult_fake [display, gray]
-  "@{term \"\<lambda>x y. x y\"}"
-  "Abs (\"x\", \"'a \<Rightarrow> 'b\", Abs (\"y\", \"'a\", Bound 1 $ Bound 0))"}
+  \<open>@{term "\<lambda>x y. x y"}\<close>
+  \<open>Abs ("x", "'a \<Rightarrow> 'b", Abs ("y", "'a", Bound 1 $ Bound 0))\<close>}
 
   the indices refer to the number of Abstractions (@{ML Abs}) that we need to
   skip until we hit the @{ML Abs} that binds the corresponding
@@ -70,25 +70,25 @@
   term shown above:
 
   @{ML_matchresult_fake [display, gray]
-"@{term \"\<lambda>x y. x y\"}
+\<open>@{term "\<lambda>x y. x y"}
   |> pretty_term @{context}
-  |> pwriteln"
-  "\<lambda>x. x"}
+  |> pwriteln\<close>
+  \<open>\<lambda>x. x\<close>}
 
   This is one common source for puzzlement in Isabelle, which has 
   tacitly eta-contracted the output. You obtain a similar result 
   with beta-redexes
 
   @{ML_matchresult_fake [display, gray]
-"let 
-  val redex = @{term \"(\<lambda>(x::int) (y::int). x)\"} 
-  val arg1 = @{term \"1::int\"} 
-  val arg2 = @{term \"2::int\"}
+\<open>let 
+  val redex = @{term "(\<lambda>(x::int) (y::int). x)"} 
+  val arg1 = @{term "1::int"} 
+  val arg2 = @{term "2::int"}
 in
   pretty_term @{context} (redex $ arg1 $ arg2)
   |> pwriteln
-end"
-  "1"}
+end\<close>
+  \<open>1\<close>}
 
   There is a dedicated configuration value for switching off tacit
   eta-contractions, namely @{ML_ind eta_contract in Syntax} (see Section
@@ -98,16 +98,16 @@
 
 
   @{ML_matchresult_fake [display, gray]
-  "let 
-  val redex = @{term \"(\<lambda>(x::int) (y::int). x)\"} 
-  val arg1 = @{term \"1::int\"} 
-  val arg2 = @{term \"2::int\"}
+  \<open>let 
+  val redex = @{term "(\<lambda>(x::int) (y::int). x)"} 
+  val arg1 = @{term "1::int"} 
+  val arg2 = @{term "2::int"}
   val ctxt = Config.put show_abbrevs false @{context}
 in
   pretty_term ctxt (redex $ arg1 $ arg2)
   |> pwriteln
-end"
-  "(\<lambda>x y. x) 1 2"}
+end\<close>
+  \<open>(\<lambda>x y. x) 1 2\<close>}
 
   Isabelle makes a distinction between \emph{free} variables (term-constructor
   @{ML Free} and written on the user level in blue colour) and
@@ -115,15 +115,15 @@
   leading question mark). Consider the following two examples
   
   @{ML_matchresult_fake [display, gray]
-"let
-  val v1 = Var ((\"x\", 3), @{typ bool})
-  val v2 = Var ((\"x1\", 3), @{typ bool})
-  val v3 = Free (\"x\", @{typ bool})
+\<open>let
+  val v1 = Var (("x", 3), @{typ bool})
+  val v2 = Var (("x1", 3), @{typ bool})
+  val v3 = Free ("x", @{typ bool})
 in
   pretty_terms @{context} [v1, v2, v3]
   |> pwriteln
-end"
-"?x3, ?x1.3, x"}
+end\<close>
+\<open>?x3, ?x1.3, x\<close>}
 
   When constructing terms, you are usually concerned with free
   variables (as mentioned earlier, you cannot construct schematic
@@ -145,19 +145,19 @@
   terms can be constructed. For example
 
   @{ML_matchresult_fake_both [display,gray]
-  "@{term \"x x\"}"
-  "Type unification failed: Occurs check!"}
+  \<open>@{term "x x"}\<close>
+  \<open>Type unification failed: Occurs check!\<close>}
 
   raises a typing error, while it is perfectly ok to construct the term
   with the raw ML-constructors:
 
   @{ML_matchresult_fake [display,gray] 
-"let
-  val omega = Free (\"x\", @{typ \"nat \<Rightarrow> nat\"}) $ Free (\"x\", @{typ nat})
+\<open>let
+  val omega = Free ("x", @{typ "nat \<Rightarrow> nat"}) $ Free ("x", @{typ nat})
 in 
   pwriteln (pretty_term @{context} omega)
-end"
-  "x x"}
+end\<close>
+  \<open>x x\<close>}
   
   Sometimes the internal representation of terms can be surprisingly different
   from what you see at the user-level, because the layers of
@@ -186,15 +186,15 @@
   usually invisible \<open>Trueprop\<close>-coercions whenever necessary. 
   Consider for example the pairs
 
-@{ML_matchresult [display,gray] "(@{term \"P x\"}, @{prop \"P x\"})" 
-"(Free (\"P\", _) $ Free (\"x\", _),
- Const (\"HOL.Trueprop\", _) $ (Free (\"P\", _) $ Free (\"x\", _)))"}
+@{ML_matchresult [display,gray] \<open>(@{term "P x"}, @{prop "P x"})\<close> 
+\<open>(Free ("P", _) $ Free ("x", _),
+ Const ("HOL.Trueprop", _) $ (Free ("P", _) $ Free ("x", _)))\<close>}
 
   where a coercion is inserted in the second component and 
 
-  @{ML_matchresult [display,gray] "(@{term \"P x \<Longrightarrow> Q x\"}, @{prop \"P x \<Longrightarrow> Q x\"})" 
-  "(Const (\"Pure.imp\", _) $ _ $ _, 
- Const (\"Pure.imp\", _) $ _ $ _)"}
+  @{ML_matchresult [display,gray] \<open>(@{term "P x \<Longrightarrow> Q x"}, @{prop "P x \<Longrightarrow> Q x"})\<close> 
+  \<open>(Const ("Pure.imp", _) $ _ $ _, 
+ Const ("Pure.imp", _) $ _ $ _)\<close>}
 
   where it is not (since it is already constructed by a meta-implication). 
   The purpose of the \<open>Trueprop\<close>-coercion is to embed formulae of
@@ -204,7 +204,7 @@
   As already seen above, types can be constructed using the antiquotation 
   \<open>@{typ _}\<close>. For example:
 
-  @{ML_matchresult_fake [display,gray] "@{typ \"bool \<Rightarrow> nat\"}" "bool \<Rightarrow> nat"}
+  @{ML_matchresult_fake [display,gray] \<open>@{typ "bool \<Rightarrow> nat"}\<close> \<open>bool \<Rightarrow> nat\<close>}
 
   The corresponding datatype is
 \<close>
@@ -216,8 +216,8 @@
 
 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
+  variables (term-constructor @{ML \<open>TFree\<close>}) and schematic
+  type variables (term-constructor @{ML \<open>TVar\<close>} 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
@@ -225,8 +225,8 @@
   Using just the antiquotation \<open>@{typ "bool"}\<close> we only see
 
   @{ML_matchresult [display, gray]
-  "@{typ \"bool\"}"
-  "bool"}
+  \<open>@{typ "bool"}\<close>
+  \<open>bool\<close>}
   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
@@ -264,14 +264,14 @@
   Now the type bool is printed out in full detail.
 
   @{ML_matchresult [display,gray]
-  "@{typ \"bool\"}"
-  "Type (\"HOL.bool\", [])"}
+  \<open>@{typ "bool"}\<close>
+  \<open>Type ("HOL.bool", [])\<close>}
 
   When printing out a list-type
   
   @{ML_matchresult [display,gray]
-  "@{typ \"'a list\"}"
-  "Type (\"List.list\", [TFree (\"'a\", [\"HOL.type\"])])"}
+  \<open>@{typ "'a list"}\<close>
+  \<open>Type ("List.list", [TFree ("'a", ["HOL.type"])])\<close>}
 
   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 
@@ -280,8 +280,8 @@
   still represented by its simple name.
 
    @{ML_matchresult [display,gray]
-  "@{typ \"bool \<Rightarrow> nat\"}"
-  "Type (\"fun\", [Type (\"HOL.bool\", []), Type (\"Nat.nat\", [])])"}
+  \<open>@{typ "bool \<Rightarrow> nat"}\<close>
+  \<open>Type ("fun", [Type ("HOL.bool", []), Type ("Nat.nat", [])])\<close>}
 
   We can restore the usual behaviour of Isabelle's pretty printer
   with the code
@@ -295,10 +295,10 @@
   the standard Isabelle way.
 
   @{ML_matchresult_fake [display, gray]
-  "@{typ \"bool\"};
-@{typ \"'a list\"}"
-  "\"bool\"
-\"'a List.list\""}
+  \<open>@{typ "bool"};
+@{typ "'a list"}\<close>
+  \<open>"bool"
+"'a List.list"\<close>}
 
   \begin{readmore}
   Types are described in detail in \isccite{sec:types}. Their
@@ -338,19 +338,19 @@
   to both functions. With @{ML make_imp} you obtain the intended term involving 
   the given arguments
 
-  @{ML_matchresult [display,gray] "make_imp @{term S} @{term T}" 
-"Const _ $ 
-  Abs (\"x\", Type (\"Nat.nat\",[]),
-    Const _ $ (Free (\"S\",_) $ _) $ (Free (\"T\",_) $ _))"}
+  @{ML_matchresult [display,gray] \<open>make_imp @{term S} @{term T}\<close> 
+\<open>Const _ $ 
+  Abs ("x", Type ("Nat.nat",[]),
+    Const _ $ (Free ("S",_) $ _) $ (Free ("T",_) $ _))\<close>}
 
   whereas with @{ML make_wrong_imp} you obtain a term involving the @{term "P"} 
   and \<open>Q\<close> from the antiquotation.
 
-  @{ML_matchresult [display,gray] "make_wrong_imp @{term S} @{term T}" 
-"Const _ $ 
-  Abs (\"x\", _,
-    Const _ $ (Const _ $ (Free (\"P\",_) $ _)) $ 
-                (Const _ $ (Free (\"Q\",_) $ _)))"}
+  @{ML_matchresult [display,gray] \<open>make_wrong_imp @{term S} @{term T}\<close> 
+\<open>Const _ $ 
+  Abs ("x", _,
+    Const _ $ (Const _ $ (Free ("P",_) $ _)) $ 
+                (Const _ $ (Free ("Q",_) $ _)))\<close>}
 
   There are a number of handy functions that are frequently used for
   constructing terms. One is the function @{ML_ind list_comb in Term}, which
@@ -359,28 +359,28 @@
 
 
 @{ML_matchresult_fake [display,gray]
-"let
-  val trm = @{term \"P::bool \<Rightarrow> bool \<Rightarrow> bool\"}
-  val args = [@{term \"True\"}, @{term \"False\"}]
+\<open>let
+  val trm = @{term "P::bool \<Rightarrow> bool \<Rightarrow> bool"}
+  val args = [@{term "True"}, @{term "False"}]
 in
   list_comb (trm, args)
-end"
-"Free (\"P\", \"bool \<Rightarrow> bool \<Rightarrow> bool\") 
-   $ Const (\"True\", \"bool\") $ Const (\"False\", \"bool\")"}
+end\<close>
+\<open>Free ("P", "bool \<Rightarrow> bool \<Rightarrow> bool") 
+   $ Const ("True", "bool") $ Const ("False", "bool")\<close>}
 
   Another handy function is @{ML_ind lambda in Term}, which abstracts a variable 
   in a term. For example
 
   @{ML_matchresult_fake [display,gray]
-"let
-  val x_nat = @{term \"x::nat\"}
-  val trm = @{term \"(P::nat \<Rightarrow> bool) x\"}
+\<open>let
+  val x_nat = @{term "x::nat"}
+  val trm = @{term "(P::nat \<Rightarrow> bool) x"}
 in
   lambda x_nat trm
-end"
-  "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"}), 
+end\<close>
+  \<open>Abs ("x", "Nat.nat", Free ("P", "bool \<Rightarrow> bool") $ Bound 0)\<close>}
+
+  In this example, @{ML lambda} produces a de Bruijn index (i.e.\ @{ML \<open>Bound 0\<close>}), 
   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 \<open>P\<close>, the variable \<open>x\<close> in \<open>P x\<close>
@@ -388,13 +388,13 @@
   as in
 
   @{ML_matchresult_fake [display,gray]
-"let
-  val x_int = @{term \"x::int\"}
-  val trm = @{term \"(P::nat \<Rightarrow> bool) x\"}
+\<open>let
+  val x_int = @{term "x::int"}
+  val trm = @{term "(P::nat \<Rightarrow> bool) x"}
 in
   lambda x_int trm
-end"
-  "Abs (\"x\", \"int\", Free (\"P\", \"nat \<Rightarrow> bool\") $ Free (\"x\", \"nat\"))"}
+end\<close>
+  \<open>Abs ("x", "int", Free ("P", "nat \<Rightarrow> bool") $ Free ("x", "nat"))\<close>}
 
   then the variable \<open>Free ("x", "nat")\<close> is \emph{not} abstracted. 
   This is a fundamental principle
@@ -407,26 +407,26 @@
   @{term y}, and @{term x} by @{term True}.
 
   @{ML_matchresult_fake [display,gray]
-"let
-  val sub1 = (@{term \"(f::nat \<Rightarrow> nat \<Rightarrow> nat) 0\"}, @{term \"y::nat \<Rightarrow> nat\"})
-  val sub2 = (@{term \"x::nat\"}, @{term \"True\"})
-  val trm = @{term \"((f::nat \<Rightarrow> nat \<Rightarrow> nat) 0) x\"}
+\<open>let
+  val sub1 = (@{term "(f::nat \<Rightarrow> nat \<Rightarrow> nat) 0"}, @{term "y::nat \<Rightarrow> nat"})
+  val sub2 = (@{term "x::nat"}, @{term "True"})
+  val trm = @{term "((f::nat \<Rightarrow> nat \<Rightarrow> nat) 0) x"}
 in
   subst_free [sub1, sub2] trm
-end"
-  "Free (\"y\", \"nat \<Rightarrow> nat\") $ Const (\"True\", \"bool\")"}
+end\<close>
+  \<open>Free ("y", "nat \<Rightarrow> nat") $ Const ("True", "bool")\<close>}
 
   As can be seen, @{ML subst_free} does not take typability into account.
   However it takes alpha-equivalence into account:
 
   @{ML_matchresult_fake [display, gray]
-"let
-  val sub = (@{term \"(\<lambda>y::nat. y)\"}, @{term \"x::nat\"})
-  val trm = @{term \"(\<lambda>x::nat. x)\"}
+\<open>let
+  val sub = (@{term "(\<lambda>y::nat. y)"}, @{term "x::nat"})
+  val trm = @{term "(\<lambda>x::nat. x)"}
 in
   subst_free [sub] trm
-end"
-  "Free (\"x\", \"nat\")"}
+end\<close>
+  \<open>Free ("x", "nat")\<close>}
 
   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
@@ -447,9 +447,9 @@
   the body of the universal quantification. For example
 
   @{ML_matchresult_fake [display, gray]
-  "strip_alls @{term \"\<forall>x y. x = (y::bool)\"}"
-"([Free (\"x\", \"bool\"), Free (\"y\", \"bool\")],
-  Const (\"op =\", _) $ Bound 1 $ Bound 0)"}
+  \<open>strip_alls @{term "\<forall>x y. x = (y::bool)"}\<close>
+\<open>([Free ("x", "bool"), Free ("y", "bool")],
+  Const ("op =", _) $ Bound 1 $ Bound 0)\<close>}
 
   Note that we produced in the body two dangling de Bruijn indices. 
   Later on we will also use the inverse function that
@@ -467,19 +467,19 @@
   loose @{ML_ind Bound in Term}s with the stripped off variables.
 
   @{ML_matchresult_fake [display, gray, linenos]
-  "let
-  val (vrs, trm) = strip_alls @{term \"\<forall>x y. x = (y::bool)\"}
+  \<open>let
+  val (vrs, trm) = strip_alls @{term "\<forall>x y. x = (y::bool)"}
 in 
   subst_bounds (rev vrs, trm) 
   |> pretty_term @{context}
   |> pwriteln
-end"
-  "x = y"}
+end\<close>
+  \<open>x = y\<close>}
 
   Note that in Line 4 we had to reverse the list of variables that @{ML
   strip_alls} returned. The reason is that the head of the list the function
-  @{ML subst_bounds} takes is the replacement for @{ML "Bound 0"}, the next
-  element for @{ML "Bound 1"} and so on. 
+  @{ML subst_bounds} takes is the replacement for @{ML \<open>Bound 0\<close>}, the next
+  element for @{ML \<open>Bound 1\<close>} and so on. 
 
   Notice also that this function might introduce name clashes, since we
   substitute just a variable with the name recorded in an abstraction. This
@@ -489,12 +489,12 @@
 
 
   @{ML_matchresult_fake [display,gray]
-  "let
-  val body = Bound 0 $ Free (\"x\", @{typ nat})
+  \<open>let
+  val body = Bound 0 $ Free ("x", @{typ nat})
 in
-  Term.dest_abs (\"x\", @{typ \"nat \<Rightarrow> bool\"}, body)
-end"
-  "(\"xa\", Free (\"xa\", \"Nat.nat \<Rightarrow> bool\") $ Free (\"x\", \"Nat.nat\"))"}
+  Term.dest_abs ("x", @{typ "nat \<Rightarrow> bool"}, body)
+end\<close>
+  \<open>("xa", Free ("xa", "Nat.nat \<Rightarrow> bool") $ Free ("x", "Nat.nat"))\<close>}
 
   Sometimes it is necessary to manipulate de Bruijn indices in terms directly.
   There are many functions to do this. We describe only two. The first,
@@ -502,13 +502,13 @@
   of the loose bound variables in a term. In the code below
 
 @{ML_matchresult_fake [display,gray]
-"@{term \"\<forall>x y z u. z = u\"}
+\<open>@{term "\<forall>x y z u. z = u"}
   |> strip_alls
   ||> incr_boundvars 2
   |> build_alls
   |> pretty_term @{context}
-  |> pwriteln"
-  "\<forall>x y z u. x = y"}
+  |> pwriteln\<close>
+  \<open>\<forall>x y z u. x = y\<close>}
 
   we first strip off the forall-quantified variables (thus creating two loose
   bound variables in the body); then we increase the indices of the loose
@@ -520,14 +520,14 @@
   contains a loose bound of a certain index. For example
 
   @{ML_matchresult_fake [gray,display]
-"let
-  val body = snd (strip_alls @{term \"\<forall>x y. x = (y::bool)\"})
+\<open>let
+  val body = snd (strip_alls @{term "\<forall>x y. x = (y::bool)"})
 in
   [loose_bvar1 (body, 0),
    loose_bvar1 (body, 1),
    loose_bvar1 (body, 2)]
-end"
-  "[true, true, false]"}
+end\<close>
+  \<open>[true, true, false]\<close>}
 
   There are also many convenient functions that construct specific HOL-terms
   in the structure @{ML_structure HOLogic}. For example @{ML_ind mk_eq in
@@ -535,13 +535,13 @@
   equality are calculated from the type of the arguments. For example
 
 @{ML_matchresult_fake [gray,display]
-"let
-  val eq = HOLogic.mk_eq (@{term \"True\"}, @{term \"False\"})
+\<open>let
+  val eq = HOLogic.mk_eq (@{term "True"}, @{term "False"})
 in
   eq |> pretty_term @{context}
      |> pwriteln
-end"
-  "True = False"}
+end\<close>
+  \<open>True = False\<close>}
 
   \begin{readmore}
   There are many functions in @{ML_file "Pure/term.ML"}, @{ML_file
@@ -569,7 +569,7 @@
 text \<open>
   will not correctly match the formula @{prop[source] "\<forall>x::nat. P x"}: 
 
-  @{ML_matchresult [display,gray] "is_all @{term \"\<forall>x::nat. P x\"}" "false"}
+  @{ML_matchresult [display,gray] \<open>is_all @{term "\<forall>x::nat. P x"}\<close> \<open>false\<close>}
 
   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 
@@ -583,7 +583,7 @@
 text \<open>
   because now
 
-  @{ML_matchresult [display,gray] "is_all @{term \"\<forall>x::nat. P x\"}" "true"}
+  @{ML_matchresult [display,gray] \<open>is_all @{term "\<forall>x::nat. P x"}\<close> \<open>true\<close>}
 
   matches correctly (the first wildcard in the pattern matches any type and the
   second any term).
@@ -598,14 +598,14 @@
 text \<open>
   Unfortunately, also this function does \emph{not} work as expected, since
 
-  @{ML_matchresult [display,gray] "is_nil @{term \"Nil\"}" "false"}
+  @{ML_matchresult [display,gray] \<open>is_nil @{term "Nil"}\<close> \<open>false\<close>}
 
   The problem is that on the ML-level the name of a constant is more
   subtle than you might expect. The function @{ML is_all} worked correctly,
   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_matchresult [display,gray] "@{term \"Nil\"}" "Const (\"List.list.Nil\", _)"}
+  by @{ML \<open>Const ("All", some_type)\<close> for some_type}. However, if you look at
+
+  @{ML_matchresult [display,gray] \<open>@{term "Nil"}\<close> \<open>Const ("List.list.Nil", _)\<close>}
 
   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
@@ -613,12 +613,12 @@
   type-classes. Consider for example the constants for @{term "zero"} and
   \mbox{@{term "times"}}:
 
-  @{ML_matchresult [display,gray] "(@{term \"0::nat\"}, @{term \"times\"})" 
- "(Const (\"Groups.zero_class.zero\", _), 
- Const (\"Groups.times_class.times\", _))"}
+  @{ML_matchresult [display,gray] \<open>(@{term "0::nat"}, @{term "times"})\<close> 
+ \<open>(Const ("Groups.zero_class.zero", _), 
+ Const ("Groups.times_class.times", _))\<close>}
 
   While you could use the complete name, for example 
-  @{ML "Const (\"List.list.Nil\", some_type)" for some_type}, for referring to or
+  @{ML \<open>Const ("List.list.Nil", some_type)\<close> for some_type}, for referring to or
   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 
@@ -637,7 +637,7 @@
   For example
 
   @{ML_matchresult [display,gray]
-  "@{type_name \"list\"}" "\"List.list\""}
+  \<open>@{type_name "list"}\<close> \<open>"List.list"\<close>}
 
   Although types of terms can often be inferred, there are many
   situations where you need to construct types manually, especially  
@@ -675,9 +675,9 @@
   Here is an example:
 
 @{ML_matchresult_fake [display,gray] 
-"map_types nat_to_int @{term \"a = (1::nat)\"}" 
-"Const (\"op =\", \"int \<Rightarrow> int \<Rightarrow> bool\")
-           $ Free (\"a\", \"int\") $ Const (\"HOL.one_class.one\", \"int\")"}
+\<open>map_types nat_to_int @{term "a = (1::nat)"}\<close> 
+\<open>Const ("op =", "int \<Rightarrow> int \<Rightarrow> bool")
+           $ Free ("a", "int") $ Const ("HOL.one_class.one", "int")\<close>}
 
   If you want to obtain the list of free type-variables of a term, you
   can use the function @{ML_ind  add_tfrees in Term} 
@@ -692,8 +692,8 @@
   call them as follows
 
   @{ML_matchresult [gray,display]
-  "Term.add_tfrees @{term \"(a, b)\"} []"
-  "[(\"'b\", [\"HOL.type\"]), (\"'a\", [\"HOL.type\"])]"}
+  \<open>Term.add_tfrees @{term "(a, b)"} []\<close>
+  \<open>[("'b", ["HOL.type"]), ("'a", ["HOL.type"])]\<close>}
 
   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
@@ -799,9 +799,9 @@
   structure @{ML_structure Vartab}.
 
   @{ML_matchresult_fake [display,gray]
-  "Vartab.dest tyenv_unif"
-  "[((\"'a\", 0), ([\"HOL.type\"], \"?'b List.list\")), 
- ((\"'b\", 0), ([\"HOL.type\"], \"nat\"))]"} 
+  \<open>Vartab.dest tyenv_unif\<close>
+  \<open>[(("'a", 0), (["HOL.type"], "?'b List.list")), 
+ (("'b", 0), (["HOL.type"], "nat"))]\<close>} 
 \<close>
 
 text_raw \<open>
@@ -833,15 +833,15 @@
 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 \<open>HOL.type\<close>. Instead of @{ML "Vartab.dest"}, we will
+  the default sort \<open>HOL.type\<close>. Instead of @{ML \<open>Vartab.dest\<close>}, 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:
 
 
   @{ML_matchresult_fake [display, gray]
-  "pretty_tyenv @{context} tyenv_unif"
-  "[?'a := ?'b list, ?'b := nat]"}
+  \<open>pretty_tyenv @{context} tyenv_unif\<close>
+  \<open>[?'a := ?'b list, ?'b := nat]\<close>}
 
   The way the unification function @{ML typ_unify in Sign} is implemented 
   using an initial type environment and initial index makes it easy to
@@ -883,8 +883,8 @@
   true. This allows us to inspect the typing environment.
 
   @{ML_matchresult_fake [display,gray]
-  "pretty_tyenv @{context} tyenv"
-  "[?'a::s1 := ?'a1::{s1, s2}, ?'b::s2 := ?'a1::{s1, s2}]"}
+  \<open>pretty_tyenv @{context} tyenv\<close>
+  \<open>[?'a::s1 := ?'a1::{s1, s2}, ?'b::s2 := ?'a1::{s1, s2}]\<close>}
 
   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
@@ -892,16 +892,16 @@
   has been increased to \<open>1\<close>.
 
   @{ML_matchresult [display,gray]
-  "index"
-  "1"}
+  \<open>index\<close>
+  \<open>1\<close>}
 
   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_matchresult_fake [display, gray]
-  "pretty_tyenv @{context} tyenv_unif"
-  "[?'a := ?'b list, ?'b := nat]"}
+  \<open>pretty_tyenv @{context} tyenv_unif\<close>
+  \<open>[?'a := ?'b list, ?'b := nat]\<close>}
 
   Observe that the type environment which the function @{ML typ_unify in
   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
@@ -912,8 +912,8 @@
   ?'b\<close>, you should use the function @{ML_ind norm_type in Envir}:
 
   @{ML_matchresult_fake [display, gray]
-  "Envir.norm_type tyenv_unif @{typ_pat \"?'a * ?'b\"}"
-  "nat list * nat"}
+  \<open>Envir.norm_type tyenv_unif @{typ_pat "?'a * ?'b"}\<close>
+  \<open>nat list * nat\<close>}
 
   Matching of types can be done with the function @{ML_ind typ_match in Sign}
   also from the structure @{ML_structure Sign}. This function returns a @{ML_type
@@ -932,16 +932,16 @@
   Printing out the calculated matcher gives
 
   @{ML_matchresult_fake [display,gray]
-  "pretty_tyenv @{context} tyenv_match"
-  "[?'a := bool list, ?'b := nat]"}
+  \<open>pretty_tyenv @{context} tyenv_match\<close>
+  \<open>[?'a := bool list, ?'b := nat]\<close>}
   
   Unlike unification, which uses the function @{ML norm_type in Envir}, 
   applying the matcher to a type needs to be done with the function
   @{ML_ind subst_type in Envir}. For example
 
   @{ML_matchresult_fake [display, gray]
-  "Envir.subst_type tyenv_match @{typ_pat \"?'a * ?'b\"}"
-  "bool list * nat"}
+  \<open>Envir.subst_type tyenv_match @{typ_pat "?'a * ?'b"}\<close>
+  \<open>bool list * nat\<close>}
 
   Be careful to observe the difference: always use
   @{ML subst_type in Envir} for matchers and @{ML norm_type in Envir} 
@@ -961,15 +961,15 @@
   @{ML norm_type in Envir} to the type \<open>?'a * ?'b\<close> we obtain
 
   @{ML_matchresult_fake [display, gray]
-  "Envir.norm_type tyenv_match' @{typ_pat \"?'a * ?'b\"}"
-  "nat list * nat"}
+  \<open>Envir.norm_type tyenv_match' @{typ_pat "?'a * ?'b"}\<close>
+  \<open>nat list * nat\<close>}
 
   which does not solve the matching problem, and if
   we apply @{ML subst_type in Envir} to the same type we obtain
 
   @{ML_matchresult_fake [display, gray]
-  "Envir.subst_type tyenv_unif @{typ_pat \"?'a * ?'b\"}"
-  "?'b list * nat"}
+  \<open>Envir.subst_type tyenv_unif @{typ_pat "?'a * ?'b"}\<close>
+  \<open>?'b list * nat\<close>}
   
   which does not solve the unification problem.
 
@@ -1024,8 +1024,8 @@
   resulting term environment is
 
   @{ML_matchresult_fake [display, gray]
-  "pretty_env @{context} fo_env"
-  "[?X := P, ?Y := \<lambda>a b. Q b a]"}
+  \<open>pretty_env @{context} fo_env\<close>
+  \<open>[?X := P, ?Y := \<lambda>a b. Q b a]\<close>}
 
   The matcher can be applied to a term using the function @{ML_ind subst_term
   in Envir} (remember the same convention for types applies to terms: @{ML
@@ -1034,14 +1034,14 @@
   which is set to empty in the example below, and a term environment.
 
   @{ML_matchresult_fake [display, gray]
-  "let
-  val trm = @{term_pat \"(?X::(nat\<Rightarrow>nat\<Rightarrow>nat)\<Rightarrow>bool) ?Y\"}
+  \<open>let
+  val trm = @{term_pat "(?X::(nat\<Rightarrow>nat\<Rightarrow>nat)\<Rightarrow>bool) ?Y"}
 in
   Envir.subst_term (Vartab.empty, fo_env) trm
   |> pretty_term @{context}
   |> pwriteln
-end"
-  "P (\<lambda>a b. Q b a)"}
+end\<close>
+  \<open>P (\<lambda>a b. Q b a)\<close>}
 
   First-order matching is useful for matching against applications and
   variables. It can also deal with abstractions and a limited form of
@@ -1051,16 +1051,16 @@
   case, first-order matching produces \<open>[?X := P]\<close>.
 
   @{ML_matchresult_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\"} 
+  \<open>let
+  val fo_pat = @{term_pat "\<lambda>y. (?X::nat\<Rightarrow>bool) y"}
+  val trm = @{term "\<lambda>x. (P::nat\<Rightarrow>bool) x"} 
   val init = (Vartab.empty, Vartab.empty) 
 in
   Pattern.first_order_match @{theory} (fo_pat, trm) init
   |> snd 
   |> pretty_env @{context} 
-end"
-  "[?X := P]"}
+end\<close>
+  \<open>[?X := P]\<close>}
 \<close>
 
 text \<open>
@@ -1076,18 +1076,18 @@
   that it is beta-normal, well-typed and has no loose bound variables.
 
   @{ML_matchresult [display, gray]
-  "let
+  \<open>let
   val trm_list = 
-        [@{term_pat \"?X\"}, @{term_pat \"a\"},
-         @{term_pat \"f (\<lambda>a b. ?X a b) c\"},
-         @{term_pat \"\<lambda>a b. (+) a b\"},
-         @{term_pat \"\<lambda>a. (+) a ?Y\"}, @{term_pat \"?X ?Y\"},
-         @{term_pat \"\<lambda>a b. ?X a b ?Y\"}, @{term_pat \"\<lambda>a. ?X a a\"},
-         @{term_pat \"?X a\"}] 
+        [@{term_pat "?X"}, @{term_pat "a"},
+         @{term_pat "f (\<lambda>a b. ?X a b) c"},
+         @{term_pat "\<lambda>a b. (+) a b"},
+         @{term_pat "\<lambda>a. (+) a ?Y"}, @{term_pat "?X ?Y"},
+         @{term_pat "\<lambda>a b. ?X a b ?Y"}, @{term_pat "\<lambda>a. ?X a a"},
+         @{term_pat "?X a"}] 
 in
   map Pattern.pattern trm_list
-end"
-  "[true, true, true, true, true, false, false, false, false]"}
+end\<close>
+  \<open>[true, true, true, true, true, false, false, false, false]\<close>}
 
   The point of the restriction to patterns is that unification and matching 
   are decidable and produce most general unifiers, respectively matchers. 
@@ -1102,15 +1102,15 @@
   @{ML_structure Pattern}. An example for higher-order pattern unification is
 
   @{ML_matchresult_fake [display, gray]
-  "let
-  val trm1 = @{term_pat \"\<lambda>x y. g (?X y x) (f (?Y x))\"}
-  val trm2 = @{term_pat \"\<lambda>u v. g u (f u)\"}
+  \<open>let
+  val trm1 = @{term_pat "\<lambda>x y. g (?X y x) (f (?Y x))"}
+  val trm2 = @{term_pat "\<lambda>u v. g u (f u)"}
   val init = Envir.empty 0
   val env = Pattern.unify (Context.Proof @{context}) (trm1, trm2) init (* FIXME: Reference to generic context *)
 in
   pretty_env @{context} (Envir.term_env env)
-end"
-  "[?X := \<lambda>y x. x, ?Y := \<lambda>x. x]"}
+end\<close>
+  \<open>[?X := \<lambda>y x. x, ?Y := \<lambda>x. x]\<close>}
 
   The function @{ML_ind "Envir.empty"} generates a record with a specified
   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
@@ -1153,27 +1153,27 @@
   We can print them out as follows.
 
   @{ML_matchresult_fake [display, gray]
-  "pretty_env @{context} (Envir.term_env un1);
+  \<open>pretty_env @{context} (Envir.term_env un1);
 pretty_env @{context} (Envir.term_env un2);
-pretty_env @{context} (Envir.term_env un3)"
-  "[?X := \<lambda>a. a, ?Y := f a]
+pretty_env @{context} (Envir.term_env un3)\<close>
+  \<open>[?X := \<lambda>a. a, ?Y := f a]
 [?X := f, ?Y := a]
-[?X := \<lambda>b. f a]"}
+[?X := \<lambda>b. f a]\<close>}
 
 
   In case of failure the function @{ML_ind unifiers in Unify} does not raise
   an exception, rather returns the empty sequence. For example
 
   @{ML_matchresult [display, gray]
-"let 
-  val trm1 = @{term \"a\"}
-  val trm2 = @{term \"b\"}
+\<open>let 
+  val trm1 = @{term "a"}
+  val trm2 = @{term "b"}
   val init = Envir.empty 0
 in
   Unify.unifiers (Context.Proof @{context}, init, [(trm1, trm2)])
   |> Seq.pull
-end"
-"NONE"}
+end\<close>
+\<open>NONE\<close>}
 
   In order to find a reasonable solution for a unification problem, Isabelle
   also tries first to solve the problem by higher-order pattern
@@ -1182,8 +1182,8 @@
   manipulated as a configuration value. For example
 
   @{ML_matchresult_fake [display,gray]
-  "Config.get_global @{theory} (Unify.search_bound)"
-  "Int 60"}
+  \<open>Config.get_global @{theory} (Unify.search_bound)\<close>
+  \<open>Int 60\<close>}
 
   If this bound is reached during unification, Isabelle prints out the
   warning message @{text [quotes] "Unification bound exceeded"} and
@@ -1267,14 +1267,14 @@
  
 
   @{ML_matchresult_fake [gray,display,linenos] 
-  "let  
+  \<open>let  
   val pat = Logic.strip_imp_concl (Thm.prop_of @{thm spec})
-  val trm = @{term \"Trueprop (Q True)\"}
+  val trm = @{term "Trueprop (Q True)"}
   val inst = matcher_inst @{context} pat trm 1
 in
   Drule.instantiate_normalize inst @{thm spec}
-end"
-  "\<forall>x. Q x \<Longrightarrow> Q True"}
+end\<close>
+  \<open>\<forall>x. Q x \<Longrightarrow> Q True\<close>}
 
   Note that we had to insert a \<open>Trueprop\<close>-coercion in Line 3 since the 
   conclusion of @{thm [source] spec} contains one.
@@ -1355,28 +1355,28 @@
   type of a term. Consider for example:
 
   @{ML_matchresult [display,gray] 
-  "type_of (@{term \"f::nat \<Rightarrow> bool\"} $ @{term \"x::nat\"})" "bool"}
+  \<open>type_of (@{term "f::nat \<Rightarrow> bool"} $ @{term "x::nat"})\<close> \<open>bool\<close>}
 
   To calculate the type, this function traverses the whole term and will
   detect any typing inconsistency. For example changing the type of the variable 
   @{term "x"} from @{typ "nat"} to @{typ "int"} will result in the error message: 
 
   @{ML_matchresult_fake [display,gray] 
-  "type_of (@{term \"f::nat \<Rightarrow> bool\"} $ @{term \"x::int\"})" 
-  "*** Exception- TYPE (\"type_of: type mismatch in application\" \<dots>"}
+  \<open>type_of (@{term "f::nat \<Rightarrow> bool"} $ @{term "x::int"})\<close> 
+  \<open>*** Exception- TYPE ("type_of: type mismatch in application" \<dots>\<close>}
 
   Since the complete traversal might sometimes be too costly and
   not necessary, there is the function @{ML_ind fastype_of in Term}, which 
   also returns the type of a term.
 
   @{ML_matchresult [display,gray] 
-  "fastype_of (@{term \"f::nat \<Rightarrow> bool\"} $ @{term \"x::nat\"})" "bool"}
+  \<open>fastype_of (@{term "f::nat \<Rightarrow> bool"} $ @{term "x::nat"})\<close> \<open>bool\<close>}
 
   However, efficiency is gained on the expense of skipping some tests. You 
   can see this in the following example
 
    @{ML_matchresult [display,gray] 
-  "fastype_of (@{term \"f::nat \<Rightarrow> bool\"} $ @{term \"x::int\"})" "bool"}
+  \<open>fastype_of (@{term "f::nat \<Rightarrow> bool"} $ @{term "x::int"})\<close> \<open>bool\<close>}
 
   where no error is detected.
 
@@ -1388,15 +1388,15 @@
   @{ML_ind check_term in Syntax}. An example is as follows:
 
   @{ML_matchresult_fake [display,gray] 
-"let
-  val c = Const (@{const_name \"plus\"}, dummyT) 
-  val o = @{term \"1::nat\"} 
-  val v = Free (\"x\", dummyT)
+\<open>let
+  val c = Const (@{const_name "plus"}, dummyT) 
+  val o = @{term "1::nat"} 
+  val v = Free ("x", dummyT)
 in   
   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\")"}
+end\<close>
+\<open>Const ("HOL.plus_class.plus", "nat \<Rightarrow> nat \<Rightarrow> nat") $
+  Const ("HOL.one_class.one", "nat") $ Free ("x", "nat")\<close>}
 
   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.
@@ -1433,67 +1433,67 @@
   write:
 
   @{ML_matchresult_fake [display,gray] 
-  "Thm.cterm_of @{context} @{term \"(a::nat) + b = c\"}" 
-  "a + b = c"}
+  \<open>Thm.cterm_of @{context} @{term "(a::nat) + b = c"}\<close> 
+  \<open>a + b = c\<close>}
 
   This can also be written with an antiquotation:
 
   @{ML_matchresult_fake [display,gray] 
-  "@{cterm \"(a::nat) + b = c\"}" 
-  "a + b = c"}
+  \<open>@{cterm "(a::nat) + b = c"}\<close> 
+  \<open>a + b = c\<close>}
 
   Attempting to obtain the certified term for
 
   @{ML_matchresult_fake_both [display,gray] 
-  "@{cterm \"1 + True\"}" 
-  "Type unification failed \<dots>"}
+  \<open>@{cterm "1 + True"}\<close> 
+  \<open>Type unification failed \<dots>\<close>}
 
   yields an error (since the term is not typable). A slightly more elaborate
   example that type-checks is:
 
 @{ML_matchresult_fake [display,gray] 
-"let
-  val natT = @{typ \"nat\"}
-  val zero = @{term \"0::nat\"}
+\<open>let
+  val natT = @{typ "nat"}
+  val zero = @{term "0::nat"}
   val plus = Const (@{const_name plus}, [natT, natT] ---> natT)
 in
   Thm.cterm_of @{context} (plus $ zero $ zero)
-end" 
-  "0 + 0"}
+end\<close> 
+  \<open>0 + 0\<close>}
 
   In Isabelle not just terms need to be certified, but also types. For example, 
   you obtain the certified type for the Isabelle type @{typ "nat \<Rightarrow> bool"} on 
   the ML-level as follows:
 
   @{ML_matchresult_fake [display,gray]
-  "Thm.ctyp_of @{context} (@{typ nat} --> @{typ bool})"
-  "nat \<Rightarrow> bool"}
+  \<open>Thm.ctyp_of @{context} (@{typ nat} --> @{typ bool})\<close>
+  \<open>nat \<Rightarrow> bool\<close>}
 
   or with the antiquotation:
 
   @{ML_matchresult_fake [display,gray]
-  "@{ctyp \"nat \<Rightarrow> bool\"}"
-  "nat \<Rightarrow> bool"}
+  \<open>@{ctyp "nat \<Rightarrow> bool"}\<close>
+  \<open>nat \<Rightarrow> bool\<close>}
 
   Since certified terms are, unlike terms, abstract objects, we cannot
   pattern-match against them. However, we can construct them. For example
   the function @{ML_ind apply in Thm} produces a certified application.
 
   @{ML_matchresult_fake [display,gray]
-  "Thm.apply @{cterm \"P::nat \<Rightarrow> bool\"} @{cterm \"3::nat\"}"
-  "P 3"}
+  \<open>Thm.apply @{cterm "P::nat \<Rightarrow> bool"} @{cterm "3::nat"}\<close>
+  \<open>P 3\<close>}
 
   Similarly the function @{ML_ind list_comb in Drule} from the structure @{ML_structure Drule}
   applies a list of @{ML_type cterm}s.
 
   @{ML_matchresult_fake [display,gray]
-  "let
-  val chead = @{cterm \"P::unit \<Rightarrow> nat \<Rightarrow> bool\"}
-  val cargs = [@{cterm \"()\"}, @{cterm \"3::nat\"}]
+  \<open>let
+  val chead = @{cterm "P::unit \<Rightarrow> nat \<Rightarrow> bool"}
+  val cargs = [@{cterm "()"}, @{cterm "3::nat"}]
 in
   Drule.list_comb (chead, cargs)
-end"
-  "P () 3"}
+end\<close>
+  \<open>P () 3\<close>}
 
   \begin{readmore}
   For functions related to @{ML_type cterm}s and @{ML_type ctyp}s see 
@@ -1547,8 +1547,8 @@
   final statement of the theorem.
 
   @{ML_matchresult_fake [display, gray]
-  "pwriteln (pretty_thm @{context} my_thm)"
-  "\<lbrakk>\<And>x. P x \<Longrightarrow> Q x; P t\<rbrakk> \<Longrightarrow> Q t"}
+  \<open>pwriteln (pretty_thm @{context} my_thm)\<close>
+  \<open>\<lbrakk>\<And>x. P x \<Longrightarrow> Q x; P t\<rbrakk> \<Longrightarrow> Q t\<close>}
 
   However, internally the code-snippet constructs the following 
   proof.
@@ -1613,12 +1613,12 @@
 
 
   @{ML_matchresult [display,gray]
-  "let
-  fun pred s = match_string \"my_thm_simp\" s
+  \<open>let
+  fun pred s = match_string "my_thm_simp" s
 in
   exists pred (get_thm_names_from_ss @{context})
-end"
-  "true"}
+end\<close>
+  \<open>true\<close>}
 
   The main point of storing the theorems @{thm [source] my_thm} and @{thm
   [source] my_thm_simp} is that they can now also be referenced with the
@@ -1717,22 +1717,22 @@
   Testing them for alpha equality produces:
 
   @{ML_matchresult [display,gray]
-"(Thm.eq_thm_prop (@{thm thm1}, @{thm thm2}),
- Thm.eq_thm_prop (@{thm thm2}, @{thm thm3}))"
-"(true, false)"}
+\<open>(Thm.eq_thm_prop (@{thm thm1}, @{thm thm2}),
+ Thm.eq_thm_prop (@{thm thm2}, @{thm thm3}))\<close>
+\<open>(true, false)\<close>}
 
   Many functions destruct theorems into @{ML_type cterm}s. For example
   the functions @{ML_ind lhs_of in Thm} and @{ML_ind rhs_of in Thm} return 
   the left and right-hand side, respectively, of a meta-equality.
 
   @{ML_matchresult_fake [display,gray]
-  "let
+  \<open>let
   val eq = @{thm True_def}
 in
   (Thm.lhs_of eq, Thm.rhs_of eq) 
   |> apply2 (Pretty.string_of o (pretty_cterm @{context}))
-end"
-  "(True, (\<lambda>x. x) = (\<lambda>x. x))"}
+end\<close>
+  \<open>(True, (\<lambda>x. x) = (\<lambda>x. x))\<close>}
 
   Other function produce terms that can be pattern-matched. 
   Suppose the following two theorems.
@@ -1746,22 +1746,22 @@
   We can destruct them into premises and conclusions as follows. 
 
  @{ML_matchresult_fake [display,gray]
-"let
+\<open>let
   val ctxt = @{context}
   fun prems_and_concl thm =
-     [[Pretty.str \"Premises:\", pretty_terms ctxt (Thm.prems_of thm)], 
-      [Pretty.str \"Conclusion:\", pretty_term ctxt (Thm.concl_of thm)]]
+     [[Pretty.str "Premises:", pretty_terms ctxt (Thm.prems_of thm)], 
+      [Pretty.str "Conclusion:", pretty_term ctxt (Thm.concl_of thm)]]
      |> map Pretty.block
      |> Pretty.chunks
      |> pwriteln
 in
   prems_and_concl @{thm foo_test1};
   prems_and_concl @{thm foo_test2}
-end"
-"Premises: ?A, ?B
+end\<close>
+\<open>Premises: ?A, ?B
 Conclusion: ?C
 Premises: 
-Conclusion: ?A \<longrightarrow> ?B \<longrightarrow> ?C"}
+Conclusion: ?A \<longrightarrow> ?B \<longrightarrow> ?C\<close>}
 
   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
@@ -1779,11 +1779,11 @@
   unfold the constant @{term "True"} according to its definition (Line 2).
 
   @{ML_matchresult_fake [display,gray,linenos]
-  "Thm.reflexive @{cterm \"True\"}
+  \<open>Thm.reflexive @{cterm "True"}
   |> Simplifier.rewrite_rule @{context} [@{thm True_def}]
   |> pretty_thm @{context}
-  |> pwriteln"
-  "(\<lambda>x. x) = (\<lambda>x. x) \<equiv> (\<lambda>x. x) = (\<lambda>x. x)"}
+  |> pwriteln\<close>
+  \<open>(\<lambda>x. x) = (\<lambda>x. x) \<equiv> (\<lambda>x. x) = (\<lambda>x. x)\<close>}
 
   Often it is necessary to transform theorems to and from the object 
   logic, that is replacing all \<open>\<longrightarrow>\<close> and \<open>\<forall>\<close> by \<open>\<Longrightarrow>\<close> 
@@ -1796,20 +1796,20 @@
   replaces all object connectives by equivalents in the meta logic. For example
 
   @{ML_matchresult_fake [display, gray]
-  "Object_Logic.rulify @{context} @{thm foo_test2}"
-  "\<lbrakk>?A; ?B\<rbrakk> \<Longrightarrow> ?C"}
+  \<open>Object_Logic.rulify @{context} @{thm foo_test2}\<close>
+  \<open>\<lbrakk>?A; ?B\<rbrakk> \<Longrightarrow> ?C\<close>}
 
   The transformation in the other direction can be achieved with function
   @{ML_ind atomize in Object_Logic} and the following code.
 
   @{ML_matchresult_fake [display,gray]
-  "let
+  \<open>let
   val thm = @{thm foo_test1}
   val meta_eq = Object_Logic.atomize @{context} (Thm.cprop_of thm)
 in
   Raw_Simplifier.rewrite_rule @{context} [meta_eq] thm
-end"
-  "?A \<longrightarrow> ?B \<longrightarrow> ?C"}
+end\<close>
+  \<open>?A \<longrightarrow> ?B \<longrightarrow> ?C\<close>}
 
   In this code the function @{ML atomize in Object_Logic} produces 
   a meta-equation between the given theorem and the theorem transformed
@@ -1838,8 +1838,8 @@
   This function produces for the theorem @{thm [source] list.induct}
 
   @{ML_matchresult_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"}
+  \<open>atomize_thm @{context} @{thm list.induct}\<close>
+  \<open>\<forall>P list. P [] \<longrightarrow> (\<forall>a list. P list \<longrightarrow> P (a # list)) \<longrightarrow> P list\<close>}
 
   Theorems can also be produced from terms by giving an explicit proof. 
   One way to achieve this is by using the function @{ML_ind prove in Goal}
@@ -1847,13 +1847,13 @@
   to prove the term @{term "P \<Longrightarrow> P"}.
   
   @{ML_matchresult_fake [display,gray]
-  "let
-  val trm = @{term \"P \<Longrightarrow> P::bool\"}
+  \<open>let
+  val trm = @{term "P \<Longrightarrow> P::bool"}
   val tac = K (assume_tac @{context} 1)
 in
-  Goal.prove @{context} [\"P\"] [] trm tac
-end"
-  "?P \<Longrightarrow> ?P"}
+  Goal.prove @{context} ["P"] [] trm tac
+end\<close>
+  \<open>?P \<Longrightarrow> ?P\<close>}
 
   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
@@ -1879,8 +1879,8 @@
   proposition.
 
   @{ML_matchresult_fake [display, gray]
-  "multi_test @{context} 3"
-  "[\"?f ?x = ?f ?x\", \"?f ?x = ?f ?x\", \"?f ?x = ?f ?x\"]"}
+  \<open>multi_test @{context} 3\<close>
+  \<open>["?f ?x = ?f ?x", "?f ?x = ?f ?x", "?f ?x = ?f ?x"]\<close>}
 
   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 \<open>3000\<close>, 
@@ -1904,8 +1904,8 @@
   reasons. An example of this function is as follows:
 
   @{ML_matchresult_fake [display, gray]
-  "Skip_Proof.make_thm @{theory} @{prop \"True = False\"}"
-  "True = False"}
+  \<open>Skip_Proof.make_thm @{theory} @{prop "True = False"}\<close>
+  \<open>True = False\<close>}
 
   \begin{readmore}
   Functions that setup goal states and prove theorems are implemented in 
@@ -1927,8 +1927,8 @@
   @{ML_ind get_tags in Thm}. So far the the auxiliary data of this lemma is 
 
   @{ML_matchresult_fake [display,gray]
-  "Thm.get_tags @{thm foo_data}"
-  "[(\"name\", \"General.foo_data\"), (\"kind\", \"lemma\")]"}
+  \<open>Thm.get_tags @{thm foo_data}\<close>
+  \<open>[("name", "General.foo_data"), ("kind", "lemma")]\<close>}
 
   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 
@@ -1945,9 +1945,9 @@
   The data of the theorem @{thm [source] foo_data'} is then as follows:
 
   @{ML_matchresult_fake [display,gray]
-  "Thm.get_tags @{thm foo_data'}"
-  "[(\"name\", \"General.foo_data'\"), (\"kind\", \"lemma\"), 
- (\"case_names\", \"foo_case_one;foo_case_two\")]"}
+  \<open>Thm.get_tags @{thm foo_data'}\<close>
+  \<open>[("name", "General.foo_data'"), ("kind", "lemma"), 
+ ("case_names", "foo_case_one;foo_case_two")]\<close>}
 
   You can observe the case names of this lemma on the user level when using 
   the proof methods \<open>cases\<close> and \<open>induct\<close>. In the proof below
@@ -2037,10 +2037,10 @@
   established theorem. This can be done with
 
   @{ML_matchresult_fake [display,gray]
-  "@{thm my_conjIa}
+  \<open>@{thm my_conjIa}
   |> Thm.proof_body_of
-  |> get_names"
-  "[\"Essential.my_conjIa\"]"}
+  |> get_names\<close>
+  \<open>["Essential.my_conjIa"]\<close>}
 
   whereby \<open>Essential\<close> refers to the theory name in which
   we established the theorem @{thm [source] my_conjIa}. The function @{ML_ind
@@ -2051,13 +2051,13 @@
   first level of the proof-tree, as follows.
 
   @{ML_matchresult_fake [display,gray]
-  "@{thm my_conjIa}
+  \<open>@{thm my_conjIa}
   |> Thm.proof_body_of
   |> get_pbodies
   |> map get_names
-  |> List.concat"
-  "[\"HOL.conjunct2\", \"HOL.conjunct1\", \"HOL.conjI\", \"Pure.protectD\", 
-  \"Pure.protectI\"]"}
+  |> List.concat\<close>
+  \<open>["HOL.conjunct2", "HOL.conjunct1", "HOL.conjI", "Pure.protectD", 
+  "Pure.protectI"]\<close>}
 
   The theorems @{thm [source] Pure.protectD} and @{thm [source]
   Pure.protectI} that are internal theorems are always part of a
@@ -2065,12 +2065,12 @@
   count as a separate theorem, as you can see in the following code.
 
   @{ML_matchresult_fake [display,gray]
-  "@{thm my_conjIb}
+  \<open>@{thm my_conjIb}
   |> Thm.proof_body_of
   |> get_pbodies
   |> map get_names
-  |> List.concat"
-  "[\"Pure.protectD\", \"Pure.protectI\"]"}
+  |> List.concat\<close>
+  \<open>["Pure.protectD", "Pure.protectI"]\<close>}
 
   Interestingly, but not surprisingly, the proof of @{thm [source]
   my_conjIc} procceeds quite differently from @{thm [source] my_conjIa}
@@ -2078,14 +2078,14 @@
   are returned for @{thm [source] my_conjIc}.
 
   @{ML_matchresult_fake [display,gray]
-  "@{thm my_conjIc}
+  \<open>@{thm my_conjIc}
   |> Thm.proof_body_of
   |> get_pbodies
   |> map get_names
-  |> List.concat"
-  "[\"HOL.Eq_TrueI\", \"HOL.simp_thms_25\", \"HOL.eq_reflection\",
-  \"HOL.conjunct2\", \"HOL.conjunct1\", \"HOL.TrueI\", \"Pure.protectD\",
-  \"Pure.protectI\"]"}
+  |> List.concat\<close>
+  \<open>["HOL.Eq_TrueI", "HOL.simp_thms_25", "HOL.eq_reflection",
+  "HOL.conjunct2", "HOL.conjunct1", "HOL.TrueI", "Pure.protectD",
+  "Pure.protectI"]\<close>}
 
   Of course we can also descend into the second level of the tree 
   ``behind'' @{thm [source] my_conjIa} say, which
@@ -2093,16 +2093,16 @@
   @{thm [source] conjunct1}, @{thm [source] conjunct2} and @{thm [source] conjI}.
 
   @{ML_matchresult_fake [display, gray]
-  "@{thm my_conjIa}
+  \<open>@{thm my_conjIa}
   |> Thm.proof_body_of
   |> get_pbodies
   |> map get_pbodies
   |> (map o map) get_names
   |> List.concat
   |> List.concat
-  |> duplicates (op=)"
-  "[\"HOL.spec\", \"HOL.and_def\", \"HOL.mp\", \"HOL.impI\", \"Pure.protectD\",
-  \"Pure.protectI\"]"}
+  |> duplicates (op=)\<close>
+  \<open>["HOL.spec", "HOL.and_def", "HOL.mp", "HOL.impI", "Pure.protectD",
+  "Pure.protectI"]\<close>}
 
   \begin{exercise}
   Have a look at the theorems that are used when a lemma is ``proved''
@@ -2309,7 +2309,7 @@
 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.}
+  @{ML \<open>Context.>> o Context.map_theory\<close>}.\footnote{\bf FIXME: explain what happens here.}
 
   As an example of a slightly more complicated theorem attribute, we implement 
   our own version of \<open>[THEN \<dots>]\<close>. This attribute will take a list of theorems
@@ -2409,8 +2409,8 @@
   then you can see it is added to the initially empty list.
 
   @{ML_matchresult_fake [display,gray]
-  "MyThms.get @{context}" 
-  "[\"True\"]"}
+  \<open>MyThms.get @{context}\<close> 
+  \<open>["True"]\<close>}
 
   You can also add theorems using the command \isacommand{declare}.
 \<close>
@@ -2423,8 +2423,8 @@
   theorem list to be updated as:
 
   @{ML_matchresult_fake [display,gray]
-  "MyThms.get @{context}"
-  "[\"True\", \"Suc (Suc 0) = 2\"]"}
+  \<open>MyThms.get @{context}\<close>
+  \<open>["True", "Suc (Suc 0) = 2"]\<close>}
 
   The theorem @{thm [source] trueI_2} only appears once, since the 
   function @{ML_ind  add_thm in Thm} tests for duplicates, before extending
@@ -2436,8 +2436,8 @@
 text \<open>After this, the theorem list is again: 
 
   @{ML_matchresult_fake [display,gray]
-  "MyThms.get @{context}"
-  "[\"True\"]"}
+  \<open>MyThms.get @{context}\<close>
+  \<open>["True"]\<close>}
 
   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
@@ -2469,7 +2469,7 @@
   type. For example
 
   @{ML_matchresult_fake [display,gray]
-  "Pretty.str \"test\"" "String (\"test\", 4)"}
+  \<open>Pretty.str "test"\<close> \<open>String ("test", 4)\<close>}
 
   where the result indicates that we transformed a string with length 4. Once
   you have a pretty type, you can, for example, control where linebreaks may
@@ -2504,20 +2504,20 @@
   we obtain the ugly output:
 
 @{ML_matchresult_fake [display,gray]
-"tracing test_str"
-"fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar foooooooooo
+\<open>tracing test_str\<close>
+\<open>fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar foooooooooo
 ooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaa
 aaaaaaar fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar fo
-oooooooooooooobaaaaaaaaaaaar"}
+oooooooooooooobaaaaaaaaaaaar\<close>}
 
   We obtain the same if we just use the function @{ML pprint}.
 
 @{ML_matchresult_fake [display,gray]
-"pprint (Pretty.str test_str)"
-"fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar foooooooooo
+\<open>pprint (Pretty.str test_str)\<close>
+\<open>fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar foooooooooo
 ooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaa
 aaaaaaar fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar fo
-oooooooooooooobaaaaaaaaaaaar"}
+oooooooooooooobaaaaaaaaaaaar\<close>}
 
   However by using pretty types you have the ability to indicate possible
   linebreaks for example at each whitespace. You can achieve this with the
@@ -2527,60 +2527,60 @@
   them with the function @{ML_ind blk in Pretty} as follows:
 
 @{ML_matchresult_fake [display,gray]
-"let
-  val ptrs = map Pretty.str (space_explode \" \" test_str)
+\<open>let
+  val ptrs = map Pretty.str (space_explode " " test_str)
 in
   pprint (Pretty.blk (0, Pretty.breaks ptrs))
-end"
-"fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar 
+end\<close>
+\<open>fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar 
 fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar 
 fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar
-fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar"}
+fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar\<close>}
 
   Here the layout of @{ML test_str} is much more pleasing to the 
-  eye. The @{ML "0"} in @{ML_ind  blk in Pretty} stands for no hanging 
+  eye. The @{ML \<open>0\<close>} in @{ML_ind  blk in Pretty} stands for no hanging 
   indentation of the printed string. You can increase the indentation 
   and obtain
   
 @{ML_matchresult_fake [display,gray]
-"let
-  val ptrs = map Pretty.str (space_explode \" \" test_str)
+\<open>let
+  val ptrs = map Pretty.str (space_explode " " test_str)
 in
   pprint (Pretty.blk (3, Pretty.breaks ptrs))
-end"
-"fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar 
+end\<close>
+\<open>fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar 
    fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar 
    fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar
-   fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar"}
+   fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar\<close>}
 
   where starting from the second line the indent is 3. If you want
   that every line starts with the same indent, you can use the
   function @{ML_ind  indent in Pretty} as follows:
 
 @{ML_matchresult_fake [display,gray]
-"let
-  val ptrs = map Pretty.str (space_explode \" \" test_str)
+\<open>let
+  val ptrs = map Pretty.str (space_explode " " test_str)
 in
   pprint (Pretty.indent 10 (Pretty.blk (0, Pretty.breaks ptrs)))
-end"
-"          fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar 
+end\<close>
+\<open>          fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar 
           fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar 
           fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar
-          fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar"}
+          fooooooooooooooobaaaaaaaaaaaar fooooooooooooooobaaaaaaaaaaaar\<close>}
 
   If you want to print out a list of items separated by commas and 
   have the linebreaks handled properly, you can use the function 
   @{ML_ind  commas in Pretty}. For example
 
 @{ML_matchresult_fake [display,gray]
-"let
+\<open>let
   val ptrs = map (Pretty.str o string_of_int) (99998 upto 100020)
 in
   pprint (Pretty.blk (0, Pretty.commas ptrs))
-end"
-"99998, 99999, 100000, 100001, 100002, 100003, 100004, 100005, 100006, 
+end\<close>
+\<open>99998, 99999, 100000, 100001, 100002, 100003, 100004, 100005, 100006, 
 100007, 100008, 100009, 100010, 100011, 100012, 100013, 100014, 100015, 
-100016, 100017, 100018, 100019, 100020"}
+100016, 100017, 100018, 100019, 100020\<close>}
 
   where @{ML upto} generates a list of integers. You can print out this
   list as a ``set'', that means enclosed inside @{text [quotes] "{"} and
@@ -2591,14 +2591,14 @@
 text \<open>
   
 @{ML_matchresult_fake [display,gray]
-"let
+\<open>let
   val ptrs = map (Pretty.str o string_of_int) (99998 upto 100020)
 in
-  pprint (Pretty.enum \",\" \"{\" \"}\" ptrs)
-end"
-"{99998, 99999, 100000, 100001, 100002, 100003, 100004, 100005, 100006, 
+  pprint (Pretty.enum "," "{" "}" ptrs)
+end\<close>
+\<open>{99998, 99999, 100000, 100001, 100002, 100003, 100004, 100005, 100006, 
   100007, 100008, 100009, 100010, 100011, 100012, 100013, 100014, 100015, 
-  100016, 100017, 100018, 100019, 100020}"}
+  100016, 100017, 100018, 100019, 100020}\<close>}
 
   As can be seen, this function prints out the ``set'' so that starting 
   from the second, each new line has an indentation of 2.
@@ -2623,58 +2623,58 @@
 
 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
+  8 the last item. We have to use @{ML \<open>Pretty.brk 1\<close>} 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
   for example
 
 @{ML_matchresult_fake [display,gray]
-"let
+\<open>let
   val ptrs1 = map (Pretty.str o string_of_int) (1 upto 22)
   val ptrs2 = map (Pretty.str o string_of_int) (10 upto 28)
 in
   pprint (Pretty.blk (0, and_list ptrs1));
   pprint (Pretty.blk (0, and_list ptrs2))
-end"
-"1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21 
+end\<close>
+\<open>1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21 
 and 22
 10, 11, 12, 13, 14, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27 and
-28"}
+28\<close>}
 
   Like @{ML blk in Pretty}, the function @{ML_ind chunks in Pretty} prints out 
   a list of items, but automatically inserts forced breaks between each item.
   Compare
 
   @{ML_matchresult_fake [display,gray]
-  "let
-  val a_and_b = [Pretty.str \"a\", Pretty.str \"b\"]
+  \<open>let
+  val a_and_b = [Pretty.str "a", Pretty.str "b"]
 in
   pprint (Pretty.blk (0, a_and_b));
   pprint (Pretty.chunks a_and_b)
-end"
-"ab
+end\<close>
+\<open>ab
 a
-b"}
+b\<close>}
 
   The function @{ML_ind big_list in Pretty} helps with printing long lists.
   It is used for example in the command \isacommand{print\_theorems}. An
   example is as follows.
 
   @{ML_matchresult_fake [display,gray]
-  "let
+  \<open>let
   val pstrs = map (Pretty.str o string_of_int) (4 upto 10)
 in
-  pprint (Pretty.big_list \"header\" pstrs)
-end"
-  "header
+  pprint (Pretty.big_list "header" pstrs)
+end\<close>
+  \<open>header
   4
   5
   6
   7
   8
   9
-  10"}
+  10\<close>}
 
   The point of the pretty-printing functions is to conveninetly obtain 
   a lay-out of terms and types that is pleasing to the eye. If we print
@@ -2682,12 +2682,12 @@
   exercise~\ref{ex:debruijn} we obtain the following: 
 
   @{ML_matchresult_fake [display,gray]
-  "pprint (Syntax.pretty_term  @{context} (de_bruijn 4))"
-  "(P 3 = P 4 \<longrightarrow> P 4 \<and> P 3 \<and> P 2 \<and> P 1) \<and>
+  \<open>pprint (Syntax.pretty_term  @{context} (de_bruijn 4))\<close>
+  \<open>(P 3 = P 4 \<longrightarrow> P 4 \<and> P 3 \<and> P 2 \<and> P 1) \<and>
 (P 2 = P 3 \<longrightarrow> P 4 \<and> P 3 \<and> P 2 \<and> P 1) \<and>
 (P 1 = P 2 \<longrightarrow> P 4 \<and> P 3 \<and> P 2 \<and> P 1) \<and> 
 (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"}
+P 4 \<and> P 3 \<and> P 2 \<and> P 1\<close>}
 
   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
@@ -2716,16 +2716,16 @@
   Now you can write
 
   @{ML_matchresult_fake [display,gray]
-  "tell_type @{context} @{term \"min (Suc 0)\"}"
-  "The term \"min (Suc 0)\" has type \"nat \<Rightarrow> nat\"."}
+  \<open>tell_type @{context} @{term "min (Suc 0)"}\<close>
+  \<open>The term "min (Suc 0)" has type "nat \<Rightarrow> nat".\<close>}
   
   To see the proper line breaking, you can try out the function on a bigger term 
   and type. For example:
 
   @{ML_matchresult_fake [display,gray]
-  "tell_type @{context} @{term \"(=) ((=) ((=) ((=) ((=) (=)))))\"}"
-  "The term \"(=) ((=) ((=) ((=) ((=) (=)))))\" has type 
-\"((((('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool\"."}
+  \<open>tell_type @{context} @{term "(=) ((=) ((=) ((=) ((=) (=)))))"}\<close>
+  \<open>The term "(=) ((=) ((=) ((=) ((=) (=)))))" has type 
+"((((('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool) \<Rightarrow> bool".\<close>}
 
   \begin{readmore}
   The general infrastructure for pretty-printing is implemented in the file
diff -r be23597e81db -r f875a25aa72d ProgTutorial/First_Steps.thy
--- a/ProgTutorial/First_Steps.thy	Fri May 17 07:29:51 2019 +0200
+++ b/ProgTutorial/First_Steps.thy	Fri May 17 10:38:01 2019 +0200
@@ -39,7 +39,7 @@
   \begin{isabelle}
   \begin{graybox}
   \isacommand{ML}~\<open>\<verbopen>\<close>\isanewline
-  \hspace{5mm}@{ML "3 + 4"}\isanewline
+  \hspace{5mm}@{ML \<open>3 + 4\<close>}\isanewline
   \<open>\<verbclose>\<close>\isanewline
   \<open>> 7\<close>\smallskip
   \end{graybox}
@@ -61,7 +61,7 @@
   \begin{isabelle}
   \isacommand{lemma}~\<open>test:\<close>\isanewline
   \isacommand{shows}~@{text [quotes] "True"}\isanewline
-  \isacommand{ML\_prf}~\<open>\<verbopen>\<close>~@{ML "writeln \"Trivial!\""}~\<open>\<verbclose>\<close>\isanewline
+  \isacommand{ML\_prf}~\<open>\<verbopen>\<close>~@{ML \<open>writeln "Trivial!"\<close>}~\<open>\<verbclose>\<close>\isanewline
   \isacommand{oops}
   \end{isabelle}
   \end{quote}
@@ -93,7 +93,7 @@
   code. This can be done in a ``quick-and-dirty'' fashion using the function
   @{ML_ind writeln in Output}. For example
 
-  @{ML_matchresult_fake [display,gray] "writeln \"any string\"" "\"any string\""}
+  @{ML_matchresult_fake [display,gray] \<open>writeln "any string"\<close> \<open>"any string"\<close>}
 
   will print out @{text [quotes] "any string"}.  
   This function expects a string as argument. If you develop under
@@ -110,9 +110,9 @@
   for example:
 
   @{ML_matchresult_fake [display,gray] 
-  "if 0 = 1 then true else (error \"foo\")" 
-"*** foo
-***"}
+  \<open>if 0 = 1 then true else (error "foo")\<close> 
+\<open>*** foo
+***\<close>}
 
   This function raises the exception \<open>ERROR\<close>, which will then 
   be displayed by the infrastructure indicating that it is an error by
@@ -137,8 +137,8 @@
   They can be used as follows
 
   @{ML_matchresult_fake [display,gray]
-  "pwriteln (pretty_term @{context} @{term \"1::nat\"})"
-  "\"1\""}
+  \<open>pwriteln (pretty_term @{context} @{term "1::nat"})\<close>
+  \<open>"1"\<close>}
 
   If there is more than one term to be printed, you can use the 
   function @{ML_ind commas in Pretty} and @{ML_ind block in Pretty} 
@@ -160,8 +160,8 @@
   Now by using this context @{ML pretty_term} prints out
 
   @{ML_matchresult_fake [display, gray]
-  "pwriteln (pretty_term show_types_ctxt @{term \"(1::nat, x)\"})"
-  "(1::nat, x::'a)"}
+  \<open>pwriteln (pretty_term show_types_ctxt @{term "(1::nat, x)"})\<close>
+  \<open>(1::nat, x::'a)\<close>}
 
   where \<open>1\<close> and \<open>x\<close> are displayed with their inferred types.
   Other configuration values that influence
@@ -204,8 +204,8 @@
   instantiation of \<open>?P\<close> and \<open>?Q\<close>. 
 
   @{ML_matchresult_fake [display, gray]
-  "pwriteln (pretty_thm @{context} @{thm conjI})"
-  "\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q"}
+  \<open>pwriteln (pretty_thm @{context} @{thm conjI})\<close>
+  \<open>\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q\<close>}
 
   However, to improve the readability when printing theorems, we
   can switch off the question marks as follows:
@@ -222,8 +222,8 @@
   With this function, theorem @{thm [source] conjI} is now printed as follows:
 
   @{ML_matchresult_fake [display, gray]
-  "pwriteln (pretty_thm_no_vars @{context} @{thm conjI})"
-  "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> P \<and> Q"}
+  \<open>pwriteln (pretty_thm_no_vars @{context} @{thm conjI})\<close>
+  \<open>\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> P \<and> Q\<close>}
   
   Again the functions @{ML commas} and @{ML block in Pretty} help 
   with printing more than one theorem. 
@@ -265,17 +265,17 @@
   \emph{not} print out information as
 
 @{ML_matchresult_fake [display,gray]
-"pwriteln (Pretty.str \"First half,\"); 
-pwriteln (Pretty.str \"and second half.\")"
-"First half,
-and second half."}
+\<open>pwriteln (Pretty.str "First half,"); 
+pwriteln (Pretty.str "and second half.")\<close>
+\<open>First half,
+and second half.\<close>}
 
   but as a single string with appropriate formatting. For example
 
 @{ML_matchresult_fake [display,gray]
-"pwriteln (Pretty.str (\"First half,\" ^ \"\\n\" ^ \"and second half.\"))"
-"First half,
-and second half."}
+\<open>pwriteln (Pretty.str ("First half," ^ "\\n" ^ "and second half."))\<close>
+\<open>First half,
+and second half.\<close>}
   
   To ease this kind of string manipulations, there are a number
   of library functions in Isabelle. For example,  the function 
@@ -283,9 +283,9 @@
   and inserts newlines in between each element. 
 
   @{ML_matchresult_fake [display, gray]
-  "pwriteln (Pretty.str (cat_lines [\"foo\", \"bar\"]))"
-  "foo
-bar"}
+  \<open>pwriteln (Pretty.str (cat_lines ["foo", "bar"]))\<close>
+  \<open>foo
+bar\<close>}
 
   Section \ref{sec:pretty} will explain the infrastructure that Isabelle 
   provides for more elaborate pretty printing. 
@@ -383,20 +383,20 @@
 
 text \<open>
   This function takes a term and a context as arguments. If the term is of function
-  type, then @{ML "apply_fresh_args"} returns the term with distinct variables 
+  type, then @{ML \<open>apply_fresh_args\<close>} returns the term with distinct variables 
   applied to it. For example, below three variables are applied to the term 
   @{term [show_types] "P::nat \<Rightarrow> int \<Rightarrow> unit \<Rightarrow> bool"}:
 
   @{ML_matchresult_fake [display,gray]
-"let
-  val trm = @{term \"P::nat \<Rightarrow> int \<Rightarrow> unit \<Rightarrow> bool\"}
+\<open>let
+  val trm = @{term "P::nat \<Rightarrow> int \<Rightarrow> unit \<Rightarrow> bool"}
   val ctxt = @{context}
 in 
   apply_fresh_args trm ctxt
    |> pretty_term ctxt
    |> pwriteln
-end" 
-  "P z za zb"}
+end\<close> 
+  \<open>P z za zb\<close>}
 
   You can read off this behaviour from how @{ML apply_fresh_args} is coded: in
   Line 2, the function @{ML_ind fastype_of in Term} calculates the type of the
@@ -415,15 +415,15 @@
   tremendously to avoid any name clashes. Consider for example:
 
    @{ML_matchresult_fake [display,gray]
-"let
-  val trm = @{term \"za::'a \<Rightarrow> 'b \<Rightarrow> 'c\"}
+\<open>let
+  val trm = @{term "za::'a \<Rightarrow> 'b \<Rightarrow> 'c"}
   val ctxt = @{context}
 in
   apply_fresh_args trm ctxt 
    |> pretty_term ctxt
    |> pwriteln
-end"
-  "za z zb"}
+end\<close>
+  \<open>za z zb\<close>}
   
   where the \<open>za\<close> is correctly avoided.
 
@@ -444,7 +444,7 @@
   \isacommand{setup}- or \isacommand{local\_setup}-command. These functions 
   have to be of type @{ML_type "theory -> theory"}, respectively 
   @{ML_type "local_theory -> local_theory"}. More than one such setup function 
-  can be composed with @{ML "#>"}. Consider for example the following code, 
+  can be composed with @{ML \<open>#>\<close>}. Consider for example the following code, 
   where we store the theorems @{thm [source] conjI}, @{thm [source] conjunct1} 
   and @{thm [source] conjunct2} under alternative names.
 \<close>  
@@ -463,7 +463,7 @@
   @{ML_ind note in Local_Theory} in the structure @{ML_structure Local_Theory}; 
   it stores a theorem under a name. 
   In lines 5 to 6 we call this function to give alternative names for the three
-  theorems. The point of @{ML "#>"} is that you can sequence such function calls. 
+  theorems. The point of @{ML \<open>#>\<close>} is that you can sequence such function calls. 
 
   The remaining combinators we describe in this section add convenience for
   the ``waterfall method'' of writing functions. The combinator @{ML_ind tap
@@ -501,9 +501,9 @@
 
 text \<open>
   which takes \<open>x\<close> as argument, and then increments \<open>x\<close>, but also keeps
-  \<open>x\<close>. The intermediate result is therefore the pair @{ML "(x + 1, x)"
+  \<open>x\<close>. The intermediate result is therefore the pair @{ML \<open>(x + 1, x)\<close>
   for x}. After that, the function increments the right-hand component of the
-  pair. So finally the result will be @{ML "(x + 1, x + 1)" for x}.
+  pair. So finally the result will be @{ML \<open>(x + 1, x + 1)\<close> for x}.
 
   The combinators @{ML_ind "|>>" in Basics} and @{ML_ind "||>" in Basics} are
   defined for functions manipulating pairs. The first applies the function to
@@ -522,8 +522,8 @@
   These two functions can, for example, be used to avoid explicit \<open>lets\<close> for
   intermediate values in functions that return pairs. As an example, suppose you
   want to separate a list of integers into two lists according to a
-  threshold. If the threshold is @{ML "5"}, the list @{ML "[1,6,2,5,3,4]"}
-  should be separated as @{ML "([1,2,3,4], [6,5])"}.  Such a function can be
+  threshold. If the threshold is @{ML \<open>5\<close>}, the list @{ML \<open>[1,6,2,5,3,4]\<close>}
+  should be separated as @{ML \<open>([1,2,3,4], [6,5])\<close>}.  Such a function can be
   implemented as
 \<close>
 
@@ -537,7 +537,7 @@
 
 text \<open>
   where the return value of the recursive call is bound explicitly to
-  the pair @{ML "(los, grs)" for los grs}. However, this function
+  the pair @{ML \<open>(los, grs)\<close> for los grs}. However, this function
   can be implemented more concisely as
 \<close>
 
@@ -588,37 +588,37 @@
   the value by one, but also nest the intermediate results to the left. For example 
 
   @{ML_matchresult [display,gray]
-  "acc_incs 1"
-  "((((\"\", 1), 2), 3), 4)"}
+  \<open>acc_incs 1\<close>
+  \<open>(((("", 1), 2), 3), 4)\<close>}
 
   You can continue this chain with:
   
   @{ML_matchresult [display,gray]
-  "acc_incs 1 ||>> (fn x => (x, x + 2))"
-  "(((((\"\", 1), 2), 3), 4), 6)"}
+  \<open>acc_incs 1 ||>> (fn x => (x, x + 2))\<close>
+  \<open>((((("", 1), 2), 3), 4), 6)\<close>}
 
   An example where this combinator is useful is as follows
 
   @{ML_matchresult_fake [display, gray]
-  "let
+  \<open>let
   val ((names1, names2), _) =
     @{context}
-    |> Variable.variant_fixes (replicate 4 \"x\")
-    ||>> Variable.variant_fixes (replicate 5 \"x\")
+    |> Variable.variant_fixes (replicate 4 "x")
+    ||>> Variable.variant_fixes (replicate 5 "x")
 in
   (names1, names2)
-end"
-  "([\"x\", \"xa\", \"xb\", \"xc\"], [\"xd\", \"xe\", \"xf\", \"xg\", \"xh\"])"}
+end\<close>
+  \<open>(["x", "xa", "xb", "xc"], ["xd", "xe", "xf", "xg", "xh"])\<close>}
 
-  Its purpose is to create nine variants of the string @{ML "\"x\""} so
+  Its purpose is to create nine variants of the string @{ML \<open>"x"\<close>} so
   that no variant will clash with another. Suppose for some reason we want
   to bind four variants to the lists @{ML_text "name1"} and the
   rest to @{ML_text "name2"}. In order to obtain non-clashing
   variants we have to thread the context through the function calls
   (the context records which variants have been previously created).
-  For the first call we can use @{ML "|>"}, but in the
+  For the first call we can use @{ML \<open>|>\<close>}, but in the
   second and any further call to @{ML_ind variant_fixes in Variable} we 
-  have to use @{ML "||>>"} in order to account for the result(s) 
+  have to use @{ML \<open>||>>\<close>} in order to account for the result(s) 
   obtained by previous calls.
   
   A more realistic example for this combinator is the following code
@@ -640,20 +640,20 @@
   the theorem corresponding to the definitions. For example for the first definition:
 
   @{ML_matchresult_fake [display, gray]
-  "let 
+  \<open>let 
   val (one_trm, (_, one_thm)) = one_def
 in
   pwriteln (pretty_term ctxt' one_trm);
   pwriteln (pretty_thm ctxt' one_thm)
-end"
-  "One
-One \<equiv> 1"}
-  Recall that @{ML "|>"} is the reverse function application. Recall also that
-  the related reverse function composition is @{ML "#>"}. In fact all the
-  combinators @{ML "|->"}, @{ML "|>>"} , @{ML "||>"} and @{ML "||>>"}
+end\<close>
+  \<open>One
+One \<equiv> 1\<close>}
+  Recall that @{ML \<open>|>\<close>} is the reverse function application. Recall also that
+  the related reverse function composition is @{ML \<open>#>\<close>}. In fact all the
+  combinators @{ML \<open>|->\<close>}, @{ML \<open>|>>\<close>} , @{ML \<open>||>\<close>} and @{ML \<open>||>>\<close>}
   described above have related combinators for function composition, namely
   @{ML_ind "#->" in Basics}, @{ML_ind "#>>" in Basics}, @{ML_ind "##>" in
-  Basics} and @{ML_ind "##>>" in Basics}. Using @{ML "#->"}, for example, the
+  Basics} and @{ML_ind "##>>" in Basics}. Using @{ML \<open>#->\<close>}, for example, the
   function \<open>double\<close> can also be written as:
 \<close>
 
@@ -667,22 +667,22 @@
   sometimes necessary to do some ``plumbing'' in order to fit functions
   together. We have already seen such plumbing in the function @{ML
   apply_fresh_args}, where @{ML curry} is needed for making the function @{ML
-  list_comb}, which works over pairs, to fit with the combinator @{ML "|>"}. Such 
+  list_comb}, which works over pairs, to fit with the combinator @{ML \<open>|>\<close>}. Such 
   plumbing is also needed in situations where a function operates over lists, 
   but one calculates only with a single element. An example is the function 
   @{ML_ind check_terms in Syntax}, whose purpose is to simultaneously type-check 
   a list of terms. Consider the code:
 
   @{ML_matchresult_fake [display, gray]
-  "let
+  \<open>let
   val ctxt = @{context}
 in
-  map (Syntax.parse_term ctxt) [\"m + n\", \"m * n\", \"m - (n::nat)\"] 
+  map (Syntax.parse_term ctxt) ["m + n", "m * n", "m - (n::nat)"] 
   |> Syntax.check_terms ctxt
   |> pretty_terms ctxt
   |> pwriteln
-end"
-  "m + n, m * n, m - n"}
+end\<close>
+  \<open>m + n, m * n, m - n\<close>}
 \<close>
 
 text \<open>
@@ -695,15 +695,15 @@
   in terms of @{ML singleton} and @{ML check_terms in Syntax}.} For example
 
   @{ML_matchresult_fake [display, gray, linenos]
-  "let 
+  \<open>let 
   val ctxt = @{context}
 in
-  Syntax.parse_term ctxt \"m - (n::nat)\" 
+  Syntax.parse_term ctxt "m - (n::nat)" 
   |> singleton (Syntax.check_terms ctxt)
   |> pretty_term ctxt
   |> pwriteln
-end"
-  "m - n"}
+end\<close>
+  \<open>m - n\<close>}
    
   where in Line 5, the function operating over lists fits with the
   single term generated in Line 4.
@@ -716,7 +716,7 @@
   \end{readmore}
 
   \begin{exercise}
-  Find out what the combinator @{ML "K I"} does.
+  Find out what the combinator @{ML \<open>K I\<close>} does.
   \end{exercise}
 \<close>
 
@@ -743,7 +743,7 @@
   are indicated by the @{ML_text @}-sign followed by text wrapped in \<open>{\<dots>}\<close>.  For example, one can print out the name of the current theory with
   the code
   
-  @{ML_matchresult [display,gray] "Context.theory_name @{theory}" "\"First_Steps\""}
+  @{ML_matchresult [display,gray] \<open>Context.theory_name @{theory}\<close> \<open>"First_Steps"\<close>}
  
   where \<open>@{theory}\<close> is an antiquotation that is substituted with the
   current theory (remember that we assumed we are inside the theory 
@@ -772,34 +772,34 @@
   defined abbreviations. For example
 
   @{ML_matchresult_fake [display, gray]
-  "Proof_Context.print_abbrevs false @{context}"
-"\<dots>
+  \<open>Proof_Context.print_abbrevs false @{context}\<close>
+\<open>\<dots>
 INTER \<equiv> INFI
 Inter \<equiv> Inf
-\<dots>"}
+\<dots>\<close>}
 
   The precise output of course depends on the abbreviations that are
   currently defined; this can change over time.
   You can also use antiquotations to refer to proved theorems: 
   \<open>@{thm \<dots>}\<close> for a single theorem
 
-  @{ML_matchresult_fake [display,gray] "@{thm allI}" "(\<And>x. ?P x) \<Longrightarrow> \<forall>x. ?P x"}
+  @{ML_matchresult_fake [display,gray] \<open>@{thm allI}\<close> \<open>(\<And>x. ?P x) \<Longrightarrow> \<forall>x. ?P x\<close>}
 
   and \<open>@{thms \<dots>}\<close> for more than one
 
 @{ML_matchresult_fake [display,gray] 
-  "@{thms conj_ac}" 
-"(?P \<and> ?Q) = (?Q \<and> ?P)
+  \<open>@{thms conj_ac}\<close> 
+\<open>(?P \<and> ?Q) = (?Q \<and> ?P)
 (?P \<and> ?Q \<and> ?R) = (?Q \<and> ?P \<and> ?R)
-((?P \<and> ?Q) \<and> ?R) = (?P \<and> ?Q \<and> ?R)"}  
+((?P \<and> ?Q) \<and> ?R) = (?P \<and> ?Q \<and> ?R)\<close>}  
 
   The thm-antiquotations can also be used for manipulating theorems. For 
   example, if you need the version of the theorem @{thm [source] refl} that 
   has a meta-equality instead of an equality, you can write
 
 @{ML_matchresult_fake [display,gray] 
-  "@{thm refl[THEN eq_reflection]}"
-  "?x \<equiv> ?x"}
+  \<open>@{thm refl[THEN eq_reflection]}\<close>
+  \<open>?x \<equiv> ?x\<close>}
 
   The point of these antiquotations is that referring to theorems in this way
   makes your code independent from what theorems the user might have stored
@@ -817,9 +817,9 @@
   The result can be printed out as follows.
 
   @{ML_matchresult_fake [gray,display]
-"foo_thms |> pretty_thms_no_vars @{context}
-         |> pwriteln"
-  "True, False \<Longrightarrow> P"}
+\<open>foo_thms |> pretty_thms_no_vars @{context}
+         |> pwriteln\<close>
+  \<open>True, False \<Longrightarrow> P\<close>}
 
   You can also refer to the current simpset via an antiquotation. To illustrate 
   this we implement the function that extracts the theorem names stored in a 
@@ -841,8 +841,8 @@
   The current simpset can be referred to using @{ML_ind simpset_of in Raw_Simplifier}.
 
   @{ML_matchresult_fake [display,gray] 
-  "get_thm_names_from_ss @{context}" 
-  "[\"Nat.of_nat_eq_id\", \"Int.of_int_eq_id\", \"Nat.One_nat_def\", \<dots>]"}
+  \<open>get_thm_names_from_ss @{context}\<close> 
+  \<open>["Nat.of_nat_eq_id", "Int.of_int_eq_id", "Nat.One_nat_def", \<dots>]\<close>}
 
   Again, this way of referencing simpsets makes you independent from additions
   of lemmas to the simpset by the user, which can potentially cause loops in your
@@ -885,8 +885,8 @@
   in more detail in later sections.) An example for this antiquotation is:
 
   @{ML_matchresult_fake [display,gray]
-  "@{term_pat \"Suc (?x::nat)\"}"
-  "Const (\"Suc\", \"nat \<Rightarrow> nat\") $ Var ((\"x\", 0), \"nat\")"}
+  \<open>@{term_pat "Suc (?x::nat)"}\<close>
+  \<open>Const ("Suc", "nat \<Rightarrow> nat") $ Var (("x", 0), "nat")\<close>}
 
   which shows the internal representation of the term \<open>Suc ?x\<close>. Similarly
   we can write an antiquotation for type patterns. Its code is
@@ -981,18 +981,18 @@
   The data can be retrieved with the projection functions defined above.
   
   @{ML_matchresult_fake [display, gray]
-"project_int (nth foo_list 0); 
-project_bool (nth foo_list 1)" 
-"13
-true"}
+\<open>project_int (nth foo_list 0); 
+project_bool (nth foo_list 1)\<close> 
+\<open>13
+true\<close>}
 
   Notice that we access the integer as an integer and the boolean as
   a boolean. If we attempt to access the integer as a boolean, then we get 
   a runtime error. 
 
   @{ML_matchresult_fake [display, gray]
-"project_bool (nth foo_list 0)"  
-"*** exception Match raised"}
+\<open>project_bool (nth foo_list 0)\<close>  
+\<open>*** exception Match raised\<close>}
 
   This runtime error is the reason why ML is still type-sound despite
   containing a universal type.
@@ -1063,8 +1063,8 @@
   Section~\ref{sec:theories}). The lookup can now be performed as follows.
 
   @{ML_matchresult_fake [display, gray]
-"lookup @{theory} \"conj\""
-"SOME \"\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q\""}
+\<open>lookup @{theory} "conj"\<close>
+\<open>SOME "\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q"\<close>}
 
   An important point to note is that these tables (and data in general)
   need to be treated in a purely functional fashion. Although
@@ -1077,8 +1077,8 @@
   and accordingly, @{ML lookup} now produces the introduction rule for @{term "True"}
   
 @{ML_matchresult_fake [display, gray]
-"lookup @{theory} \"conj\""
-"SOME \"True\""}
+\<open>lookup @{theory} "conj"\<close>
+\<open>SOME "True"\<close>}
 
   there are no references involved. This is one of the most fundamental
   coding conventions for programming in Isabelle. References  
@@ -1096,11 +1096,11 @@
 
 text \<open>
   We initialise the reference with the empty list. Consequently a first 
-  lookup produces @{ML "ref []" in Unsynchronized}.
+  lookup produces @{ML \<open>ref []\<close> in Unsynchronized}.
 
   @{ML_matchresult_fake [display,gray]
-  "WrongRefData.get @{theory}"
-  "ref []"}
+  \<open>WrongRefData.get @{theory}\<close>
+  \<open>ref []\<close>}
 
   For updating the reference we use the following function
 \<close>
@@ -1118,23 +1118,23 @@
 
 text \<open>
   A lookup in the current theory gives then the expected list 
-  @{ML "ref [1]" in Unsynchronized}.
+  @{ML \<open>ref [1]\<close> in Unsynchronized}.
 
   @{ML_matchresult_fake [display,gray]
-  "WrongRefData.get @{theory}"
-  "ref [1]"}
+  \<open>WrongRefData.get @{theory}\<close>
+  \<open>ref [1]\<close>}
 
   So far everything is as expected. But, the trouble starts if we attempt to
   backtrack to the ``point'' before the \isacommand{setup}-command. There, we
   would expect that the list is empty again. But since it is stored in a
   reference, Isabelle has no control over it. So it is not empty, but still
-  @{ML "ref [1]" in Unsynchronized}. Adding to the trouble, if we execute the
-  \isacommand{setup}-command again, we do not obtain @{ML "ref [1]" in
+  @{ML \<open>ref [1]\<close> in Unsynchronized}. Adding to the trouble, if we execute the
+  \isacommand{setup}-command again, we do not obtain @{ML \<open>ref [1]\<close> in
   Unsynchronized}, but
 
   @{ML_matchresult_fake [display,gray]
-  "WrongRefData.get @{theory}"
-  "ref [1, 1]"}
+  \<open>WrongRefData.get @{theory}\<close>
+  \<open>ref [1, 1]\<close>}
 
   Now imagine how often you go backwards and forwards in your proof 
   scripts.\footnote{The same problem can be triggered in the Jedit GUI by
@@ -1180,22 +1180,22 @@
   \<open>@{context}\<close> and update it in various ways. 
 
   @{ML_matchresult_fake [display,gray]
-"let
+\<open>let
   val ctxt0 = @{context}
-  val ctxt1 = ctxt0 |> update @{term \"False\"}
-                    |> update @{term \"True \<and> True\"} 
-  val ctxt2 = ctxt0 |> update @{term \"1::nat\"}
-  val ctxt3 = ctxt2 |> update @{term \"2::nat\"}
+  val ctxt1 = ctxt0 |> update @{term "False"}
+                    |> update @{term "True \<and> True"} 
+  val ctxt2 = ctxt0 |> update @{term "1::nat"}
+  val ctxt3 = ctxt2 |> update @{term "2::nat"}
 in
   print ctxt0; 
   print ctxt1;
   print ctxt2;
   print ctxt3
-end"
-"Empty!
+end\<close>
+\<open>Empty!
 True \<and> True, False
 1
-2, 1"}
+2, 1\<close>}
 
   Many functions in Isabelle manage and update data in a similar
   fashion. Consequently, such calculations with contexts occur frequently in
@@ -1272,8 +1272,8 @@
   @{ML FooRules.get}:
 
   @{ML_matchresult_fake [display,gray] 
-  "FooRules.get @{context}" 
-  "[\"True\", \"?C\",\"?B\"]"}
+  \<open>FooRules.get @{context}\<close> 
+  \<open>["True", "?C","?B"]\<close>}
 
   Note that this function takes a proof context as argument. This might be 
   confusing, since the theorem list is stored as theory data. It becomes clear by knowing
@@ -1309,30 +1309,30 @@
   function @{ML_ind get in Config} from a proof context
 
   @{ML_matchresult [display,gray] 
-  "Config.get @{context} bval" 
-  "true"}
+  \<open>Config.get @{context} bval\<close> 
+  \<open>true\<close>}
 
   or directly from a theory using the function @{ML_ind get_global in Config}
 
   @{ML_matchresult [display,gray] 
-  "Config.get_global @{theory} bval" 
-  "true"}
+  \<open>Config.get_global @{theory} bval\<close> 
+  \<open>true\<close>}
 
   It is also possible to manipulate the configuration values
   from the ML-level with the functions @{ML_ind put in Config}
   and @{ML_ind put_global in Config}. For example
 
   @{ML_matchresult [display,gray]
-  "let
+  \<open>let
   val ctxt = @{context}
-  val ctxt' = Config.put sval \"foo\" ctxt
-  val ctxt'' = Config.put sval \"bar\" ctxt'
+  val ctxt' = Config.put sval "foo" ctxt
+  val ctxt'' = Config.put sval "bar" ctxt'
 in
   (Config.get ctxt sval, 
    Config.get ctxt' sval, 
    Config.get ctxt'' sval)
-end"
-  "(\"some string\", \"foo\", \"bar\")"}
+end\<close>
+  \<open>("some string", "foo", "bar")\<close>}
 
   A concrete example for a configuration value is 
   @{ML_ind simp_trace in Raw_Simplifier}, which switches on trace information
diff -r be23597e81db -r f875a25aa72d ProgTutorial/Intro.thy
--- a/ProgTutorial/Intro.thy	Fri May 17 07:29:51 2019 +0200
+++ b/ProgTutorial/Intro.thy	Fri May 17 10:38:01 2019 +0200
@@ -152,7 +152,7 @@
   \begin{isabelle}
   \begin{graybox}
   \isacommand{ML}~\<open>\<verbopen>\<close>\isanewline
-  \hspace{5mm}@{ML "3 + 4"}\isanewline
+  \hspace{5mm}@{ML \<open>3 + 4\<close>}\isanewline
   \<open>\<verbclose>\<close>
   \end{graybox}
   \end{isabelle}
@@ -163,13 +163,13 @@
   the enclosing \isacommand{ML}~\<open>\<verbopen> \<dots> \<verbclose>\<close> and just
   write:
 
-  @{ML [display,gray] "3 + 4"}
+  @{ML [display,gray] \<open>3 + 4\<close>}
   
   Whenever appropriate we also show the response the code 
   generates when evaluated. This response is prefixed with a 
   @{text [quotes] ">"}, like:
 
-  @{ML_matchresult [display,gray] "3 + 4" "7"}
+  @{ML_matchresult [display,gray] \<open>3 + 4\<close> \<open>7\<close>}
 
   The user-level commands of Isabelle (i.e., the non-ML code) are written
   in \isacommand{bold face} (e.g., \isacommand{lemma}, \isacommand{apply},
diff -r be23597e81db -r f875a25aa72d ProgTutorial/Package/Ind_Code.thy
--- a/ProgTutorial/Package/Ind_Code.thy	Fri May 17 07:29:51 2019 +0200
+++ b/ProgTutorial/Package/Ind_Code.thy	Fri May 17 10:38:01 2019 +0200
@@ -494,13 +494,13 @@
   the quantifiers in this theorem with @{term a}, @{term b} and @{term c} as follows:
 
   @{ML_matchresult_fake [display, gray]
-"let
-  val ctrms = [@{cterm \"a::nat\"}, @{cterm \"b::nat\"}, @{cterm \"c::nat\"}]
+\<open>let
+  val ctrms = [@{cterm "a::nat"}, @{cterm "b::nat"}, @{cterm "c::nat"}]
   val new_thm = all_elims ctrms @{thm all_elims_test}
 in
   pwriteln (pretty_thm_no_vars @{context} new_thm)
-end"
-  "P a b c"}
+end\<close>
+  \<open>P a b c\<close>}
 
   Note the difference with @{ML inst_spec_tac} from Page~\pageref{fun:instspectac}:
   @{ML inst_spec_tac} is a tactic which operates on a goal state; in contrast
@@ -511,12 +511,12 @@
   @{thm [source] imp_elims_test}:
 
   @{ML_matchresult_fake [display, gray]
-"let
+\<open>let
   val res = imp_elims @{thms imp_elims_test'} @{thm imp_elims_test}
 in
   pwriteln (pretty_thm_no_vars @{context} res)
-end"
-  "C"}
+end\<close>
+  \<open>C\<close>}
 
   Now we set up the proof for the introduction rule as follows:
 \<close>
@@ -728,7 +728,7 @@
   whether we are in the simple or complicated case by checking whether
   the topmost connective is an \<open>\<forall>\<close>. The premises in the simple
   case cannot have such a quantification, since the first step 
-  of @{ML "expand_tac"} was to ``rulify'' the lemma. 
+  of @{ML \<open>expand_tac\<close>} was to ``rulify'' the lemma. 
   The premise of the complicated case must have at least one  \<open>\<forall>\<close>
   coming from the quantification over the \<open>preds\<close>. So 
   we can implement the following function
@@ -1011,7 +1011,7 @@
   any name.} Line 21 registers the induction principles. For this we have
   to use some specific attributes. The first @{ML_ind  case_names in Rule_Cases} 
   corresponds to the case names that are used by Isar to reference the proof
-  obligations in the induction. The second @{ML "consumes 1" in Rule_Cases}
+  obligations in the induction. The second @{ML \<open>consumes 1\<close> in Rule_Cases}
   indicates that the first premise of the induction principle (namely
   the predicate over which the induction proceeds) is eliminated. 
 
diff -r be23597e81db -r f875a25aa72d ProgTutorial/Package/Ind_Interface.thy
--- a/ProgTutorial/Package/Ind_Interface.thy	Fri May 17 07:29:51 2019 +0200
+++ b/ProgTutorial/Package/Ind_Interface.thy	Fri May 17 10:38:01 2019 +0200
@@ -108,20 +108,20 @@
   of @{term even} and @{term odd}
 
   @{ML_matchresult [display,gray]
-"let
+\<open>let
   val input = filtered_input
-     (\"even and odd \" ^  
-      \"where \" ^
-      \"  even0[intro]: \\\"even 0\\\" \" ^ 
-      \"| evenS[intro]: \\\"odd n \<Longrightarrow> even (Suc n)\\\" \" ^ 
-      \"| oddS[intro]:  \\\"even n \<Longrightarrow> odd (Suc n)\\\" \")
+     ("even and odd " ^  
+      "where " ^
+      "  even0[intro]: \"even 0\" " ^ 
+      "| evenS[intro]: \"odd n \<Longrightarrow> even (Suc n)\" " ^ 
+      "| oddS[intro]:  \"even n \<Longrightarrow> odd (Suc n)\" ")
 in
   parse spec_parser input
-end"
-"(([(even, NONE, NoSyn), (odd, NONE, NoSyn)],
+end\<close>
+\<open>(([(even, NONE, NoSyn), (odd, NONE, NoSyn)],
      [((even0,_), _),
       ((evenS,_), _),
-      ((oddS,_), _)]), [])"}
+      ((oddS,_), _)]), [])\<close>}
 
   then we get back the specifications of the predicates (with type and syntax annotations), 
   and specifications of the introduction rules. This is all the information we
diff -r be23597e81db -r f875a25aa72d ProgTutorial/Parsing.thy
--- a/ProgTutorial/Parsing.thy	Fri May 17 07:29:51 2019 +0200
+++ b/ProgTutorial/Parsing.thy	Fri May 17 10:38:01 2019 +0200
@@ -60,18 +60,18 @@
   the rest of the input list. For example:
 
   @{ML_matchresult [display,gray] 
-  "($$ \"h\") (Symbol.explode \"hello\")" "(\"h\", [\"e\", \"l\", \"l\", \"o\"])"}
+  \<open>($$ "h") (Symbol.explode "hello")\<close> \<open>("h", ["e", "l", "l", "o"])\<close>}
 
   @{ML_matchresult [display,gray] 
-  "($$ \"w\") (Symbol.explode \"world\")" "(\"w\", [\"o\", \"r\", \"l\", \"d\"])"}
+  \<open>($$ "w") (Symbol.explode "world")\<close> \<open>("w", ["o", "r", "l", "d"])\<close>}
 
-  The function @{ML "$$"} will either succeed (as in the two examples above)
+  The function @{ML \<open>$$\<close>} will either succeed (as in the two examples above)
   or raise the exception \<open>FAIL\<close> if no string can be consumed. For
   example trying to parse
 
   @{ML_matchresult_fake [display,gray] 
-  "($$ \"x\") (Symbol.explode \"world\")" 
-  "Exception FAIL raised"}
+  \<open>($$ "x") (Symbol.explode "world")\<close> 
+  \<open>Exception FAIL raised\<close>}
   
   will raise the exception \<open>FAIL\<close>. The function @{ML_ind "$$" in Scan} will also
   fail if you try to consume more than a single character.
@@ -84,7 +84,7 @@
   \item \<open>MORE\<close> indicates that there is not enough input for the parser. For example 
   in \<open>($$ "h") []\<close>.
   \item \<open>ABORT\<close> indicates that a dead end is reached. 
-  It is used for example in the function @{ML "!!"} (see below).
+  It is used for example in the function @{ML \<open>!!\<close>} (see below).
   \end{itemize}
 
   However, note that these exceptions are private to the parser and cannot be accessed
@@ -98,15 +98,15 @@
   Isabelle. To see the difference consider
 
 @{ML_matchresult_fake [display,gray]
-"let 
-  val input = \"\<foo> bar\"
+\<open>let 
+  val input = "\<foo> bar"
 in
   (String.explode input, Symbol.explode input)
-end"
-"([\"\\\", \"<\", \"f\", \"o\", \"o\", \">\", \" \", \"b\", \"a\", \"r\"],
- [\"\<foo>\", \" \", \"b\", \"a\", \"r\"])"}
+end\<close>
+\<open>(["\\", "<", "f", "o", "o", ">", " ", "b", "a", "r"],
+ ["\<foo>", " ", "b", "a", "r"])\<close>}
 
-  Slightly more general than the parser @{ML "$$"} is the function 
+  Slightly more general than the parser @{ML \<open>$$\<close>} is the function 
   @{ML_ind one in Scan}, in that it takes a predicate as argument and 
   then parses exactly
   one item from the input list satisfying this predicate. For example the
@@ -114,22 +114,22 @@
   [quotes] "w"}:
 
 @{ML_matchresult [display,gray] 
-"let 
-  val hw = Scan.one (fn x => x = \"h\" orelse x = \"w\")
-  val input1 = Symbol.explode \"hello\"
-  val input2 = Symbol.explode \"world\"
+\<open>let 
+  val hw = Scan.one (fn x => x = "h" orelse x = "w")
+  val input1 = Symbol.explode "hello"
+  val input2 = Symbol.explode "world"
 in
   (hw input1, hw input2)
-end"
-    "((\"h\", [\"e\", \"l\", \"l\", \"o\"]),(\"w\", [\"o\", \"r\", \"l\", \"d\"]))"}
+end\<close>
+    \<open>(("h", ["e", "l", "l", "o"]),("w", ["o", "r", "l", "d"]))\<close>}
 
   Two parsers can be connected in sequence by using the function @{ML_ind "--" in Scan}. 
   For example parsing \<open>h\<close>, \<open>e\<close> and \<open>l\<close> (in this 
   order) you can achieve by:
 
   @{ML_matchresult [display,gray] 
-  "($$ \"h\" -- $$ \"e\" -- $$ \"l\") (Symbol.explode \"hello\")"
-  "(((\"h\", \"e\"), \"l\"), [\"l\", \"o\"])"}
+  \<open>($$ "h" -- $$ "e" -- $$ "l") (Symbol.explode "hello")\<close>
+  \<open>((("h", "e"), "l"), ["l", "o"])\<close>}
 
   Note how the result of consumed strings builds up on the left as nested pairs.  
 
@@ -137,24 +137,24 @@
   then you can use the function @{ML_ind this_string in Scan}.
 
   @{ML_matchresult [display,gray] 
-  "Scan.this_string \"hell\" (Symbol.explode \"hello\")"
-  "(\"hell\", [\"o\"])"}
+  \<open>Scan.this_string "hell" (Symbol.explode "hello")\<close>
+  \<open>("hell", ["o"])\<close>}
 
   Parsers that explore alternatives can be constructed using the function 
-  @{ML_ind  "||" in Scan}. The parser @{ML "(p || q)" for p q} returns the
+  @{ML_ind  "||" in Scan}. The parser @{ML \<open>(p || q)\<close> for p q} returns the
   result of \<open>p\<close>, in case it succeeds; otherwise it returns the
   result of \<open>q\<close>. For example:
 
 
 @{ML_matchresult [display,gray] 
-"let 
-  val hw = $$ \"h\" || $$ \"w\"
-  val input1 = Symbol.explode \"hello\"
-  val input2 = Symbol.explode \"world\"
+\<open>let 
+  val hw = $$ "h" || $$ "w"
+  val input1 = Symbol.explode "hello"
+  val input2 = Symbol.explode "world"
 in
   (hw input1, hw input2)
-end"
-  "((\"h\", [\"e\", \"l\", \"l\", \"o\"]), (\"w\", [\"o\", \"r\", \"l\", \"d\"]))"}
+end\<close>
+  \<open>(("h", ["e", "l", "l", "o"]), ("w", ["o", "r", "l", "d"]))\<close>}
 
   The functions @{ML_ind "|--" in Scan} and @{ML_ind "--|" in Scan} work like the sequencing
   function for parsers, except that they discard the item being parsed by the
@@ -163,95 +163,95 @@
   For example:
   
 @{ML_matchresult [display,gray]
-"let 
-  val just_e = $$ \"h\" |-- $$ \"e\" 
-  val just_h = $$ \"h\" --| $$ \"e\" 
-  val input = Symbol.explode \"hello\"  
+\<open>let 
+  val just_e = $$ "h" |-- $$ "e" 
+  val just_h = $$ "h" --| $$ "e" 
+  val input = Symbol.explode "hello"  
 in 
   (just_e input, just_h input)
-end"
-  "((\"e\", [\"l\", \"l\", \"o\"]), (\"h\", [\"l\", \"l\", \"o\"]))"}
+end\<close>
+  \<open>(("e", ["l", "l", "o"]), ("h", ["l", "l", "o"]))\<close>}
 
-  The parser @{ML "Scan.optional p x" for p x} returns the result of the parser 
+  The parser @{ML \<open>Scan.optional p x\<close> for p x} returns the result of the parser 
   \<open>p\<close>, in case it succeeds; otherwise it returns 
   the default value \<open>x\<close>. For example:
 
 @{ML_matchresult [display,gray]
-"let 
-  val p = Scan.optional ($$ \"h\") \"x\"
-  val input1 = Symbol.explode \"hello\"
-  val input2 = Symbol.explode \"world\"  
+\<open>let 
+  val p = Scan.optional ($$ "h") "x"
+  val input1 = Symbol.explode "hello"
+  val input2 = Symbol.explode "world"  
 in 
   (p input1, p input2)
-end" 
- "((\"h\", [\"e\", \"l\", \"l\", \"o\"]), (\"x\", [\"w\", \"o\", \"r\", \"l\", \"d\"]))"}
+end\<close> 
+ \<open>(("h", ["e", "l", "l", "o"]), ("x", ["w", "o", "r", "l", "d"]))\<close>}
 
   The function @{ML_ind option in Scan} works similarly, except no default value can
   be given. Instead, the result is wrapped as an \<open>option\<close>-type. For example:
 
 @{ML_matchresult [display,gray]
-"let 
-  val p = Scan.option ($$ \"h\")
-  val input1 = Symbol.explode \"hello\"
-  val input2 = Symbol.explode \"world\"  
+\<open>let 
+  val p = Scan.option ($$ "h")
+  val input1 = Symbol.explode "hello"
+  val input2 = Symbol.explode "world"  
 in 
   (p input1, p input2)
-end" "((SOME \"h\", [\"e\", \"l\", \"l\", \"o\"]), (NONE, [\"w\", \"o\", \"r\", \"l\", \"d\"]))"}
+end\<close> \<open>((SOME "h", ["e", "l", "l", "o"]), (NONE, ["w", "o", "r", "l", "d"]))\<close>}
 
   The function @{ML_ind ahead in Scan} parses some input, but leaves the original
   input unchanged. For example:
 
   @{ML_matchresult [display,gray]
-  "Scan.ahead (Scan.this_string \"foo\") (Symbol.explode \"foo\")" 
-  "(\"foo\", [\"f\", \"o\", \"o\"])"} 
+  \<open>Scan.ahead (Scan.this_string "foo") (Symbol.explode "foo")\<close> 
+  \<open>("foo", ["f", "o", "o"])\<close>} 
 
   The function @{ML_ind "!!" in Scan} helps with producing appropriate error messages
   during parsing. For example if you want to parse \<open>p\<close> immediately 
   followed by \<open>q\<close>, or start a completely different parser \<open>r\<close>,
   you might write:
 
-  @{ML [display,gray] "(p -- q) || r" for p q r}
+  @{ML [display,gray] \<open>(p -- q) || r\<close> for p q r}
 
   However, this parser is problematic for producing a useful error
-  message, if the parsing of @{ML "(p -- q)" for p q} fails. Because with the
+  message, if the parsing of @{ML \<open>(p -- q)\<close> for p q} fails. Because with the
   parser above you lose the information that \<open>p\<close> should be followed by \<open>q\<close>.
   To see this assume that \<open>p\<close> is present in the input, but it is not
-  followed by \<open>q\<close>. That means @{ML "(p -- q)" for p q} will fail and
+  followed by \<open>q\<close>. That means @{ML \<open>(p -- q)\<close> for p q} will fail and
   hence the alternative parser \<open>r\<close> will be tried. However, in many
   circumstances this will be the wrong parser for the input ``\<open>p\<close>-followed-by-something''
   and therefore will also fail. The error message is then caused by the failure
   of \<open>r\<close>, not by the absence of \<open>q\<close> in the input. Such
-  situation can be avoided when using the function @{ML "!!"}.  This function
+  situation can be avoided when using the function @{ML \<open>!!\<close>}.  This function
   aborts the whole process of parsing in case of a failure and prints an error
   message. For example if you invoke the parser
 
 
-  @{ML [display,gray] "!! (fn _ => fn _ =>\"foo\") ($$ \"h\")"}
+  @{ML [display,gray] \<open>!! (fn _ => fn _ =>"foo") ($$ "h")\<close>}
 
   on @{text [quotes] "hello"}, the parsing succeeds
 
   @{ML_matchresult [display,gray] 
-  "(!! (fn _ => fn _ => \"foo\") ($$ \"h\")) (Symbol.explode \"hello\")" 
-  "(\"h\", [\"e\", \"l\", \"l\", \"o\"])"}
+  \<open>(!! (fn _ => fn _ => "foo") ($$ "h")) (Symbol.explode "hello")\<close> 
+  \<open>("h", ["e", "l", "l", "o"])\<close>}
 
   but if you invoke it on @{text [quotes] "world"}
 
-  @{ML_matchresult_fake [display,gray] "(!! (fn _ => fn _ => \"foo\") ($$ \"h\")) (Symbol.explode \"world\")"
-                               "Exception ABORT raised"}
+  @{ML_matchresult_fake [display,gray] \<open>(!! (fn _ => fn _ => "foo") ($$ "h")) (Symbol.explode "world")\<close>
+                               \<open>Exception ABORT raised\<close>}
 
   then the parsing aborts and the error message \<open>foo\<close> is printed. In order to
   see the error message properly, you need to prefix the parser with the function 
   @{ML_ind error in Scan}. For example:
 
   @{ML_matchresult_fake [display,gray] 
-  "Scan.error (!! (fn _ => fn _ => \"foo\") ($$ \"h\")) (Symbol.explode \"world\")"
-  "Exception Error \"foo\" raised"}
+  \<open>Scan.error (!! (fn _ => fn _ => "foo") ($$ "h")) (Symbol.explode "world")\<close>
+  \<open>Exception Error "foo" raised\<close>}
 
   This kind of ``prefixing'' to see the correct error message is usually done by wrappers 
   such as @{ML_ind local_theory in Outer_Syntax} 
   (see Section~\ref{sec:newcommand} which explains this function in more detail). 
   
-  Let us now return to our example of parsing @{ML "(p -- q) || r" for p q
+  Let us now return to our example of parsing @{ML \<open>(p -- q) || r\<close> for p q
   r}. If you want to generate the correct error message for failure
   of parsing \<open>p\<close>-followed-by-\<open>q\<close>, then you have to write:
 \<close>
@@ -269,21 +269,21 @@
   @{text [quotes] "h"}, @{text [quotes] "e"} and @{text [quotes] "w"}, and 
   the input @{text [quotes] "holle"} 
 
-  @{ML_matchresult_fake [display,gray] "Scan.error (p_followed_by_q \"h\" \"e\" \"w\") (Symbol.explode \"holle\")"
-                               "Exception ERROR \"h is not followed by e\" raised"} 
+  @{ML_matchresult_fake [display,gray] \<open>Scan.error (p_followed_by_q "h" "e" "w") (Symbol.explode "holle")\<close>
+                               \<open>Exception ERROR "h is not followed by e" raised\<close>} 
 
   produces the correct error message. Running it with
  
-  @{ML_matchresult [display,gray] "Scan.error (p_followed_by_q \"h\" \"e\" \"w\") (Symbol.explode \"wworld\")"
-                          "((\"w\", \"w\"), [\"o\", \"r\", \"l\", \"d\"])"}
+  @{ML_matchresult [display,gray] \<open>Scan.error (p_followed_by_q "h" "e" "w") (Symbol.explode "wworld")\<close>
+                          \<open>(("w", "w"), ["o", "r", "l", "d"])\<close>}
   
   yields the expected parsing. 
 
-  The function @{ML "Scan.repeat p" for p} will apply a parser \<open>p\<close> as 
+  The function @{ML \<open>Scan.repeat p\<close> for p} will apply a parser \<open>p\<close> as 
   long as it succeeds. For example:
   
-  @{ML_matchresult [display,gray] "Scan.repeat ($$ \"h\") (Symbol.explode \"hhhhello\")" 
-                "([\"h\", \"h\", \"h\", \"h\"], [\"e\", \"l\", \"l\", \"o\"])"}
+  @{ML_matchresult [display,gray] \<open>Scan.repeat ($$ "h") (Symbol.explode "hhhhello")\<close> 
+                \<open>(["h", "h", "h", "h"], ["e", "l", "l", "o"])\<close>}
   
   Note that @{ML_ind repeat in Scan} stores the parsed items in a list. The function
   @{ML_ind repeat1 in Scan} is similar, but requires that the parser \<open>p\<close> 
@@ -294,8 +294,8 @@
   the wrapper @{ML_ind finite in Scan} and the ``stopper-token'' 
   @{ML_ind stopper in Symbol}. With them you can write:
   
-  @{ML_matchresult [display,gray] "Scan.finite Symbol.stopper (Scan.repeat ($$ \"h\")) (Symbol.explode \"hhhh\")" 
-                "([\"h\", \"h\", \"h\", \"h\"], [])"}
+  @{ML_matchresult [display,gray] \<open>Scan.finite Symbol.stopper (Scan.repeat ($$ "h")) (Symbol.explode "hhhh")\<close> 
+                \<open>(["h", "h", "h", "h"], [])\<close>}
 
   The function @{ML stopper in Symbol} is the ``end-of-input'' indicator for parsing strings;
   other stoppers need to be used when parsing, for example, tokens. However, this kind of 
@@ -305,13 +305,13 @@
   string as in
 
   @{ML_matchresult [display,gray] 
-"let 
+\<open>let 
    val p = Scan.repeat (Scan.one Symbol.not_eof)
-   val input = Symbol.explode \"foo bar foo\"
+   val input = Symbol.explode "foo bar foo"
 in
    Scan.finite Symbol.stopper p input
-end" 
-"([\"f\", \"o\", \"o\", \" \", \"b\", \"a\", \"r\", \" \", \"f\", \"o\", \"o\"], [])"}
+end\<close> 
+\<open>(["f", "o", "o", " ", "b", "a", "r", " ", "f", "o", "o"], [])\<close>}
 
   where the function @{ML_ind not_eof in Symbol} ensures that we do not read beyond the 
   end of the input string (i.e.~stopper symbol).
@@ -319,13 +319,13 @@
   The function @{ML_ind unless in Scan} takes two parsers: if the first one can 
   parse the input, then the whole parser fails; if not, then the second is tried. Therefore
   
-  @{ML_matchresult_fake_both [display,gray] "Scan.unless ($$ \"h\") ($$ \"w\") (Symbol.explode \"hello\")"
-                               "Exception FAIL raised"}
+  @{ML_matchresult_fake_both [display,gray] \<open>Scan.unless ($$ "h") ($$ "w") (Symbol.explode "hello")\<close>
+                               \<open>Exception FAIL raised\<close>}
 
   fails, while
 
-  @{ML_matchresult [display,gray] "Scan.unless ($$ \"h\") ($$ \"w\") (Symbol.explode \"world\")"
-                          "(\"w\",[\"o\", \"r\", \"l\", \"d\"])"}
+  @{ML_matchresult [display,gray] \<open>Scan.unless ($$ "h") ($$ "w") (Symbol.explode "world")\<close>
+                          \<open>("w",["o", "r", "l", "d"])\<close>}
 
   succeeds. 
 
@@ -334,43 +334,43 @@
   example below the marker symbol is a @{text [quotes] "*"}.
 
   @{ML_matchresult [display,gray]
-"let 
-  val p = Scan.repeat (Scan.unless ($$ \"*\") (Scan.one Symbol.not_eof))
-  val input1 = Symbol.explode \"fooooo\"
-  val input2 = Symbol.explode \"foo*ooo\"
+\<open>let 
+  val p = Scan.repeat (Scan.unless ($$ "*") (Scan.one Symbol.not_eof))
+  val input1 = Symbol.explode "fooooo"
+  val input2 = Symbol.explode "foo*ooo"
 in
   (Scan.finite Symbol.stopper p input1, 
    Scan.finite Symbol.stopper p input2)
-end"
-"(([\"f\", \"o\", \"o\", \"o\", \"o\", \"o\"], []),
- ([\"f\", \"o\", \"o\"], [\"*\", \"o\", \"o\", \"o\"]))"}
+end\<close>
+\<open>((["f", "o", "o", "o", "o", "o"], []),
+ (["f", "o", "o"], ["*", "o", "o", "o"]))\<close>}
 
   
   After parsing is done, you almost always want to apply a function to the parsed 
   items. One way to do this is the function @{ML_ind ">>" in Scan} where 
-  @{ML "(p >> f)" for p f} runs 
+  @{ML \<open>(p >> f)\<close> for p f} runs 
   first the parser \<open>p\<close> and upon successful completion applies the 
   function \<open>f\<close> to the result. For example
 
 @{ML_matchresult [display,gray]
-"let 
+\<open>let 
   fun double (x, y) = (x ^ x, y ^ y) 
-  val parser = $$ \"h\" -- $$ \"e\"
+  val parser = $$ "h" -- $$ "e"
 in
-  (parser >> double) (Symbol.explode \"hello\")
-end"
-"((\"hh\", \"ee\"), [\"l\", \"l\", \"o\"])"}
+  (parser >> double) (Symbol.explode "hello")
+end\<close>
+\<open>(("hh", "ee"), ["l", "l", "o"])\<close>}
 
   doubles the two parsed input strings; or
 
   @{ML_matchresult [display,gray] 
-"let 
+\<open>let 
    val p = Scan.repeat (Scan.one Symbol.not_eof)
-   val input = Symbol.explode \"foo bar foo\" 
+   val input = Symbol.explode "foo bar foo" 
 in
    Scan.finite Symbol.stopper (p >> implode) input
-end" 
-"(\"foo bar foo\",[])"}
+end\<close> 
+\<open>("foo bar foo",[])\<close>}
 
   where the single-character strings in the parsed output are transformed
   back into one string.
@@ -380,8 +380,8 @@
   untouched. For example
 
 @{ML_matchresult [display,gray]
-"Scan.lift ($$ \"h\" -- $$ \"e\") (1, Symbol.explode \"hello\")"
-"((\"h\", \"e\"), (1, [\"l\", \"l\", \"o\"]))"}
+\<open>Scan.lift ($$ "h" -- $$ "e") (1, Symbol.explode "hello")\<close>
+\<open>(("h", "e"), (1, ["l", "l", "o"]))\<close>}
 
   \footnote{\bf FIXME: In which situations is \<open>lift\<close> useful? Give examples.} 
 
@@ -426,8 +426,8 @@
   loop, even if it is called without any input. For example
 
   @{ML_matchresult_fake_both [display, gray]
-  "parse_tree \"A\""
-  "*** Exception- TOPLEVEL_ERROR raised"}
+  \<open>parse_tree "A"\<close>
+  \<open>*** Exception- TOPLEVEL_ERROR raised\<close>}
 
   raises an exception indicating that the stack limit is reached. Such
   looping parser are not useful, because of ML's strict evaluation of
@@ -450,20 +450,19 @@
   exactly the parser what we wanted. An example is as follows:
 
   @{ML_matchresult [display, gray]
-  "let
-  val input = Symbol.explode \"(A,((A))),A\"
+  \<open>let
+  val input = Symbol.explode "(A,((A))),A"
 in
-  Scan.finite Symbol.stopper (parse_tree \"A\") input
-end"
-  "(Br (Br (Lf \"A\", Lf \"A\"), Lf \"A\"), [])"}
+  Scan.finite Symbol.stopper (parse_tree "A") input
+end\<close>
+  \<open>(Br (Br (Lf "A", Lf "A"), Lf "A"), [])\<close>}
 
 
   \begin{exercise}\label{ex:scancmts}
   Write a parser that parses an input string so that any comment enclosed
   within \<open>(*\<dots>*)\<close> is replaced by the same comment but enclosed within
   \<open>(**\<dots>**)\<close> in the output string. To enclose a string, you can use the
-  function @{ML "enclose s1 s2 s" for s1 s2 s} which produces the string @{ML
-  "s1 ^ s ^ s2" for s1 s2 s}. Hint: To simplify the task ignore the proper 
+  function @{ML \<open>enclose s1 s2 s\<close> for s1 s2 s} which produces the string @{ML \<open>s1 ^ s ^ s2\<close> for s1 s2 s}. Hint: To simplify the task ignore the proper 
   nesting of comments.
   \end{exercise}
 \<close>
@@ -497,7 +496,7 @@
   token parsers take into account the kind of tokens. The first example shows
   how to generate a token list out of a string using the function 
   @{ML_ind explode in Token}. It is given the argument 
-  @{ML "Position.none"} since,
+  @{ML \<open>Position.none\<close>} since,
   at the moment, we are not interested in generating precise error
   messages. The following code
 
@@ -524,11 +523,11 @@
 text \<open>
   then lexing @{text [quotes] "hello world"} will produce
 
-  @{ML_matchresult_fake [display,gray] "Token.explode 
-  (Thy_Header.get_keywords' @{context}) Position.none \"hello world\"" 
-"[Token (_,(Keyword, \"hello\"),_), 
- Token (_,(Space, \" \"),_), 
- Token (_,(Ident, \"world\"),_)]"}
+  @{ML_matchresult_fake [display,gray] \<open>Token.explode 
+  (Thy_Header.get_keywords' @{context}) Position.none "hello world"\<close> 
+\<open>[Token (_,(Keyword, "hello"),_), 
+ Token (_,(Space, " "),_), 
+ Token (_,(Ident, "world"),_)]\<close>}
 
   Many parsing functions later on will require white space, comments and the like
   to have already been filtered out.  So from now on we are going to use the 
@@ -536,12 +535,12 @@
   For example:
 
 @{ML_matchresult_fake [display,gray]
-"let
-   val input = Token.explode (Thy_Header.get_keywords' @{context}) Position.none \"hello world\"
+\<open>let
+   val input = Token.explode (Thy_Header.get_keywords' @{context}) Position.none "hello world"
 in
    filter Token.is_proper input
-end" 
-"[Token (_,(Ident, \"hello\"), _), Token (_,(Ident, \"world\"), _)]"}
+end\<close> 
+\<open>[Token (_,(Ident, "hello"), _), Token (_,(Ident, "world"), _)]\<close>}
 
   For convenience we define the function:
 \<close>
@@ -554,10 +553,10 @@
   If you now parse
 
 @{ML_matchresult_fake [display,gray] 
-"filtered_input \"inductive | for\"" 
-"[Token (_,(Command, \"inductive\"),_), 
- Token (_,(Keyword, \"|\"),_), 
- Token (_,(Keyword, \"for\"),_)]"}
+\<open>filtered_input "inductive | for"\<close> 
+\<open>[Token (_,(Command, "inductive"),_), 
+ Token (_,(Keyword, "|"),_), 
+ Token (_,(Keyword, "for"),_)]\<close>}
 
   you obtain a list consisting of only one command and two keyword tokens.
   If you want to see which keywords and commands are currently known to Isabelle, 
@@ -569,47 +568,47 @@
   The parser @{ML_ind "$$$" in Parse} parses a single keyword. For example:
 
 @{ML_matchresult [display,gray]
-"let 
-  val input1 = filtered_input \"where for\"
-  val input2 = filtered_input \"| in\"
+\<open>let 
+  val input1 = filtered_input "where for"
+  val input2 = filtered_input "| in"
 in 
-  (Parse.$$$ \"where\" input1, Parse.$$$ \"|\" input2)
-end"
-"((\"where\",_), (\"|\",_))"}
+  (Parse.$$$ "where" input1, Parse.$$$ "|" input2)
+end\<close>
+\<open>(("where",_), ("|",_))\<close>}
 
   Any non-keyword string can be parsed with the function @{ML_ind reserved in Parse}.
   For example:
 
   @{ML_matchresult [display,gray]
-"let 
-  val p = Parse.reserved \"bar\"
-  val input = filtered_input \"bar\"
+\<open>let 
+  val p = Parse.reserved "bar"
+  val input = filtered_input "bar"
 in
   p input
-end"
-  "(\"bar\",[])"}
+end\<close>
+  \<open>("bar",[])\<close>}
 
-  Like before, you can sequentially connect parsers with @{ML "--"}. For example: 
+  Like before, you can sequentially connect parsers with @{ML \<open>--\<close>}. For example: 
 
 @{ML_matchresult [display,gray]
-"let 
-  val input = filtered_input \"| in\"
+\<open>let 
+  val input = filtered_input "| in"
 in 
-  (Parse.$$$ \"|\" -- Parse.$$$ \"in\") input
-end"
-"((\"|\", \"in\"), [])"}
+  (Parse.$$$ "|" -- Parse.$$$ "in") input
+end\<close>
+\<open>(("|", "in"), [])\<close>}
 
-  The parser @{ML "Parse.enum s p" for s p} parses a possibly empty 
+  The parser @{ML \<open>Parse.enum s p\<close> for s p} parses a possibly empty 
   list of items recognised by the parser \<open>p\<close>, where the items being parsed
   are separated by the string \<open>s\<close>. For example:
 
 @{ML_matchresult [display,gray]
-"let 
-  val input = filtered_input \"in | in | in foo\"
+\<open>let 
+  val input = filtered_input "in | in | in foo"
 in 
-  (Parse.enum \"|\" (Parse.$$$ \"in\")) input
-end" 
-"([\"in\", \"in\", \"in\"], [_])"}
+  (Parse.enum "|" (Parse.$$$ "in")) input
+end\<close> 
+\<open>(["in", "in", "in"], [_])\<close>}
 
   The function @{ML_ind enum1 in Parse} works similarly, except that the
   parsed list must be non-empty. Note that we had to add a string @{text
@@ -619,13 +618,13 @@
   ``stopper-token'' @{ML Token.stopper}. We can write:
 
 @{ML_matchresult [display,gray]
-"let 
-  val input = filtered_input \"in | in | in\"
-  val p = Parse.enum \"|\" (Parse.$$$ \"in\")
+\<open>let 
+  val input = filtered_input "in | in | in"
+  val p = Parse.enum "|" (Parse.$$$ "in")
 in 
   Scan.finite Token.stopper p input
-end" 
-"([\"in\", \"in\", \"in\"], [])"}
+end\<close> 
+\<open>(["in", "in", "in"], [])\<close>}
 
   The following function will help to run examples.
 \<close>
@@ -634,20 +633,19 @@
 
 text \<open>
   The function @{ML_ind "!!!" in Parse} can be used to force termination
-  of the parser in case of a dead end, just like @{ML "Scan.!!"} (see previous
-  section). A difference, however, is that the error message of @{ML
-  "Parse.!!!"} is fixed to be @{text [quotes] "Outer syntax error"}
+  of the parser in case of a dead end, just like @{ML \<open>Scan.!!\<close>} (see previous
+  section). A difference, however, is that the error message of @{ML \<open>Parse.!!!\<close>} is fixed to be @{text [quotes] "Outer syntax error"}
   together with a relatively precise description of the failure. For example:
 
 @{ML_matchresult_fake [display,gray]
-"let 
-  val input = filtered_input \"in |\"
-  val parse_bar_then_in = Parse.$$$ \"|\" -- Parse.$$$ \"in\"
+\<open>let 
+  val input = filtered_input "in |"
+  val parse_bar_then_in = Parse.$$$ "|" -- Parse.$$$ "in"
 in 
   parse (Parse.!!! parse_bar_then_in) input 
-end"
-"Exception ERROR \"Outer syntax error: keyword \"|\" expected, 
-but keyword in was found\" raised"
+end\<close>
+\<open>Exception ERROR "Outer syntax error: keyword "|" expected, 
+but keyword in was found" raised\<close>
 }
 
   \begin{exercise} (FIXME)
@@ -672,9 +670,9 @@
   where we pretend the parsed string starts on line 7. An example is
 
 @{ML_matchresult_fake [display,gray]
-"filtered_input' \"foo \\n bar\""
-"[Token ((\"foo\", ({line=7, end_line=7}, {line=7})), (Ident, \"foo\"), _),
- Token ((\"bar\", ({line=8, end_line=8}, {line=8})), (Ident, \"bar\"), _)]"}
+\<open>filtered_input' "foo \\n bar"\<close>
+\<open>[Token (("foo", ({line=7, end_line=7}, {line=7})), (Ident, "foo"), _),
+ Token (("bar", ({line=8, end_line=8}, {line=8})), (Ident, "bar"), _)]\<close>}
 
   in which the @{text [quotes] "\\n"} causes the second token to be in 
   line 8.
@@ -683,12 +681,12 @@
   position and return it as part of the parser result. For example
 
 @{ML_matchresult_fake [display,gray]
-"let
-  val input = filtered_input' \"where\"
+\<open>let
+  val input = filtered_input' "where"
 in 
-  parse (Parse.position (Parse.$$$ \"where\")) input
-end"
-"((\"where\", {line=7, end_line=7}), [])"}
+  parse (Parse.position (Parse.$$$ "where")) input
+end\<close>
+\<open>(("where", {line=7, end_line=7}), [])\<close>}
 
   \begin{readmore}
   The functions related to positions are implemented in the file
@@ -754,12 +752,12 @@
   be parsed using the function @{ML_ind term in Parse}. For example:
 
 @{ML_matchresult_fake [display,gray]
-"let 
-  val input = Token.explode (Thy_Header.get_keywords' @{context}) Position.none \"foo\"
+\<open>let 
+  val input = Token.explode (Thy_Header.get_keywords' @{context}) Position.none "foo"
 in 
   Parse.term input
-end"
-"(\"<markup>\", [])"}
+end\<close>
+\<open>("<markup>", [])\<close>}
 
 
   The function @{ML_ind prop in Parse} is similar, except that it gives a different
@@ -767,15 +765,15 @@
   the parsed string, but also some markup information. You can decode the
   information with the function @{ML_ind parse in YXML} in @{ML_structure YXML}. 
   The result of the decoding is an XML-tree. You can see better what is going on if
-  you replace @{ML Position.none} by @{ML "Position.line 42"}, say:
+  you replace @{ML Position.none} by @{ML \<open>Position.line 42\<close>}, say:
 
 @{ML_matchresult_fake [display,gray]
-"let 
-  val input = Token.explode (Thy_Header.get_keywords' @{context}) (Position.line 42) \"foo\"
+\<open>let 
+  val input = Token.explode (Thy_Header.get_keywords' @{context}) (Position.line 42) "foo"
 in 
   YXML.parse (fst (Parse.term input))
-end"
-"Elem (\"token\", [(\"line\", \"42\"), (\"end_line\", \"42\")], [XML.Text \"foo\"])"}
+end\<close>
+\<open>Elem ("token", [("line", "42"), ("end_line", "42")], [XML.Text "foo"])\<close>}
 
   The positional information is stored as part of an XML-tree so that code 
   called later on will be able to give more precise error messages. 
@@ -833,20 +831,20 @@
   definition of @{term even} and @{term odd}:
 
 @{ML_matchresult [display,gray]
-"let
+\<open>let
   val input = filtered_input
-     (\"even and odd \" ^  
-      \"where \" ^
-      \"  even0[intro]: \\\"even 0\\\" \" ^ 
-      \"| evenS[intro]: \\\"odd n \<Longrightarrow> even (Suc n)\\\" \" ^ 
-      \"| oddS[intro]:  \\\"even n \<Longrightarrow> odd (Suc n)\\\"\")
+     ("even and odd " ^  
+      "where " ^
+      "  even0[intro]: \"even 0\" " ^ 
+      "| evenS[intro]: \"odd n \<Longrightarrow> even (Suc n)\" " ^ 
+      "| oddS[intro]:  \"even n \<Longrightarrow> odd (Suc n)\"")
 in
   parse spec_parser input
-end"
-"(([(even, NONE, NoSyn), (odd, NONE, NoSyn)],
+end\<close>
+\<open>(([(even, NONE, NoSyn), (odd, NONE, NoSyn)],
    [((even0,_),_),
     ((evenS,_),_),
-    ((oddS,_),_)]), [])"}
+    ((oddS,_),_)]), [])\<close>}
 \<close>
 
 ML \<open>let
@@ -865,19 +863,19 @@
   \isacommand{and}-separated 
   list of variables that can include optional type annotations and syntax translations. 
   For example:\footnote{Note that in the code we need to write 
-  \<open>\"int \<Rightarrow> bool\"\<close> in order to properly escape the double quotes
+  \<open>"int \<Rightarrow> bool"\<close> in order to properly escape the double quotes
   in the compound type.}
 
 @{ML_matchresult_fake [display,gray]
-"let
+\<open>let
   val input = filtered_input 
-        \"foo::\\\"int \<Rightarrow> bool\\\" and bar::nat (\\\"BAR\\\" 100) and blonk\"
+        "foo::\"int \<Rightarrow> bool\" and bar::nat (\"BAR\" 100) and blonk"
 in
   parse Parse.vars input
-end"
-"([(foo, SOME _, NoSyn), 
-  (bar, SOME _, Mixfix (Source {text=\"BAR\",...}, [], 100, _)), 
-  (blonk, NONE, NoSyn)],[])"}  
+end\<close>
+\<open>([(foo, SOME _, NoSyn), 
+  (bar, SOME _, Mixfix (Source {text="BAR",...}, [], 100, _)), 
+  (blonk, NONE, NoSyn)],[])\<close>}  
 \<close>
 
 text \<open>
@@ -899,12 +897,12 @@
   parsed by @{ML_ind prop in Parse}. However, they can include an optional
   theorem name plus some attributes. For example
 
-@{ML_matchresult [display,gray] "let 
-  val input = filtered_input \"foo_lemma[intro,dest!]:\"
-  val ((name, attrib), _) = parse (Parse_Spec.thm_name \":\") input 
+@{ML_matchresult [display,gray] \<open>let 
+  val input = filtered_input "foo_lemma[intro,dest!]:"
+  val ((name, attrib), _) = parse (Parse_Spec.thm_name ":") input 
 in 
   (name, map Token.name_of_src attrib)
-end" "(foo_lemma, [(\"intro\", _), (\"dest\", _)])"}
+end\<close> \<open>(foo_lemma, [("intro", _), ("dest", _)])\<close>}
  
   The function @{ML_ind opt_thm_name in Parse_Spec} is the ``optional'' variant of
   @{ML_ind thm_name in Parse_Spec}. Theorem names can contain attributes. The name 
@@ -1019,7 +1017,7 @@
   behaviour of the command. In the code above we used a
   ``do-nothing''-function, which because of the parser @{ML_ind succeed in Scan}
   does not parse any argument, but immediately returns the simple
-  function @{ML "Local_Theory.background_theory I"}. We can replace
+  function @{ML \<open>Local_Theory.background_theory I\<close>}. We can replace
   this code by a function that first parses a proposition (using the
   parser @{ML Parse.prop}), then prints out some tracing information
   (using the function \<open>trace_prop\<close>) and finally does
@@ -1051,8 +1049,7 @@
   ``open up'' a proof in order to prove the proposition (for example
   \isacommand{lemma}) or prove some other properties (for example
   \isacommand{function}). To achieve this kind of behaviour, you have to use
-  the kind indicator @{ML_ind thy_goal in Keyword} and the function @{ML
-  "local_theory_to_proof" in Outer_Syntax} to set up the command. 
+  the kind indicator @{ML_ind thy_goal in Keyword} and the function @{ML \<open>local_theory_to_proof\<close> in Outer_Syntax} to set up the command. 
   Below we show the command \isacommand{foobar\_goal} which takes a
   proposition as argument and then starts a proof in order to prove
   it. Therefore, we need to announce this command in the header 
@@ -1084,7 +1081,7 @@
   @{ML_ind read_prop in Syntax}, which converts a string into a proper proposition.
   In Line 6 the function @{ML_ind theorem in Proof} starts the proof for the
   proposition. Its argument @{ML NONE} stands for a locale (which we chose to
-  omit); the argument @{ML "(K I)"} stands for a function that determines what
+  omit); the argument @{ML \<open>(K I)\<close>} stands for a function that determines what
   should be done with the theorem once it is proved (we chose to just forget
   about it). 
 
diff -r be23597e81db -r f875a25aa72d ProgTutorial/Readme.thy
--- a/ProgTutorial/Readme.thy	Fri May 17 07:29:51 2019 +0200
+++ b/ProgTutorial/Readme.thy	Fri May 17 10:38:01 2019 +0200
@@ -39,7 +39,7 @@
   The following antiquotations are defined:
 
   \begin{itemize}
-  \item[$\bullet$] \<open>@{ML "expr" for vars in structs}\<close> should be used
+  \item[$\bullet$] \<open>@{ML \<open>expr\<close> for vars in structs}\<close> should be used
   for displaying any ML-ex\-pression, because the antiquotation checks whether
   the expression is valid ML-code. The \<open>for\<close>- and \<open>in\<close>-arguments are optional. The former is used for evaluating open
   expressions by giving a list of free variables. The latter is used to
@@ -48,23 +48,23 @@
   
   \begin{center}\small
   \begin{tabular}{lll}
-  \<open>@{ML "1 + 3"}\<close>         &                 & @{ML "1 + 3"}\\
-  \<open>@{ML "a + b" for a b}\<close> & \;\;produce\;\; & @{ML "a + b" for a b}\\
-  \<open>@{ML Ident in OuterLex}\<close> &                 & @{ML Ident in OuterLex}\\
+  \<open>@{ML \<open>1 + 3\<close>}\<close>         &                 & @{ML \<open>1 + 3\<close>}\\
+  \<open>@{ML \<open>a + b\<close> for a b}\<close> & \;\;produce\;\; & @{ML \<open>a + b\<close> for a b}\\
+  \<open>@{ML explode in Symbol}\<close> &                 & @{ML explode in Symbol}\\
   \end{tabular}
   \end{center}
 
-  \item[$\bullet$] \<open>@{ML_matchresult "expr" "pat"}\<close> should be used to
+  \item[$\bullet$] \<open>@{ML_matchresult \<open>expr\<close> \<open>pat\<close>}\<close> should be used to
   display ML-expressions and their response.  The first expression is checked
-  like in the antiquotation \<open>@{ML "expr"}\<close>; the second is a pattern
+  like in the antiquotation \<open>@{ML \<open>expr\<close>}\<close>; the second is a pattern
   that specifies the result the first expression produces. This pattern can
   contain @{text [quotes] "\<dots>"} for parts that you like to omit. The response of the
   first expression will be checked against this pattern. Examples are:
 
   \begin{center}\small
   \begin{tabular}{l}
-  \<open>@{ML_matchresult "1+2" "3"}\<close>\\
-  \<open>@{ML_matchresult "(1+2,3)" "(3,\<dots>)"}\<close>
+  \<open>@{ML_matchresult \<open>1+2\<close> \<open>3\<close>}\<close>\\
+  \<open>@{ML_matchresult \<open>(1+2,3)\<close> \<open>(3,\<dots>)\<close>}\<close>
   \end{tabular}
   \end{center}
 
@@ -72,8 +72,8 @@
 
   \begin{center}\small
   \begin{tabular}{p{3cm}p{3cm}}
-  @{ML_matchresult "1+2" "3"} &  
-  @{ML_matchresult "(1+2,3)" "(3,\<dots>)"}
+  @{ML_matchresult \<open>1+2\<close> \<open>3\<close>} &  
+  @{ML_matchresult \<open>(1+2,3)\<close> \<open>(3,_)\<close>}
   \end{tabular}
   \end{center}
   
@@ -82,16 +82,16 @@
   an abstract datatype (like @{ML_type thm} or @{ML_type cterm}).
 
   \item[$\bullet$] \<open>@{ML_matchresult_fake "expr" "pat"}\<close> works just
-  like the antiquotation \<open>@{ML_matchresult "expr" "pat"}\<close> above,
+  like the antiquotation \<open>@{ML_matchresult \<open>expr\<close> \<open>pat\<close>}\<close> above,
   except that the result-specification is not checked. Use this antiquotation
   when the result cannot be constructed or the code generates an
   exception. Examples are:
 
   \begin{center}\small
   \begin{tabular}{ll}
-  \<open>@{ML_matchresult_fake\<close> & \<open>"cterm_of @{theory} @{term \"a + b = c\"}"}\<close>\\
+  \<open>@{ML_matchresult_fake\<close> & \<open>"cterm_of @{theory} @{term "a + b = c"}"}\<close>\\
                                & \<open>"a + b = c"}\<close>\smallskip\\ 
-  \<open>@{ML_matchresult_fake\<close> & \<open>"($$ \"x\") (explode \"world\")"\<close>\\ 
+  \<open>@{ML_matchresult_fake\<close> & \<open>"($$ "x") (explode "world")"\<close>\\ 
                                & \<open>"Exception FAIL raised"}\<close>
   \end{tabular}
   \end{center}
@@ -100,8 +100,8 @@
 
   \begin{center}\small
   \begin{tabular}{p{7.2cm}}
-  @{ML_matchresult_fake "cterm_of @{theory} @{term \"a + b = c\"}" "a + b = c"}\smallskip\\
-  @{ML_matchresult_fake "($$ \"x\") (explode \"world\")" "Exception FAIL raised"}
+  @{ML_matchresult_fake \<open>Thm.cterm_of @{context} @{term "a + b = c"}\<close> \<open>a + b = c\<close>}\smallskip\\
+  @{ML_matchresult_fake \<open>($$ "x") (Symbol.explode "world")\<close> \<open>Exception FAIL raised\<close>}
   \end{tabular}
   \end{center}
   
@@ -114,7 +114,7 @@
 
   \begin{center}\small
   \begin{tabular}{ll}
-  \<open>@{ML_matchresult_fake_both\<close> & \<open>"@{cterm \"1 + True\"}"\<close>\\
+  \<open>@{ML_matchresult_fake_both\<close> & \<open>"@{cterm "1 + True"}"\<close>\\
                                     & \<open>"Type unification failed \<dots>"}\<close>
   \end{tabular}
   \end{center}
@@ -123,20 +123,20 @@
   referring to a file. It checks whether the file exists.  An example
   is 
 
-  @{text [display] "@{ML_file \"Pure/General/basics.ML\"}"}
+  @{text [display] \<open>@{ML_file "Pure/General/basics.ML"}\<close>}
   \end{itemize}
 
   The listed antiquotations honour options including \<open>[display]\<close> and 
   \<open>[quotes]\<close>. For example
 
   \begin{center}\small
-  \<open>@{ML [quotes] "\"foo\" ^ \"bar\""}\<close> \;\;produces\;\; @{text [quotes] "foobar"}
+  \<open>@{ML [quotes] \<open>"foo" ^ "bar"\<close>}\<close> \;\;produces\;\; @{text [quotes] "foobar"}
   \end{center}
 
   whereas
   
   \begin{center}\small
-  \<open>@{ML "\"foo\" ^ \"bar\""}\<close> \;\;produces only\;\; \<open>foobar\<close>
+  \<open>@{ML \<open>"foo" ^ "bar"\<close>}\<close> \;\;produces only\;\; \<open>foobar\<close>
   \end{center}
   
   \item Functions and value bindings cannot be defined inside antiquotations; they need
diff -r be23597e81db -r f875a25aa72d ProgTutorial/Recipes/Antiquotes.thy
--- a/ProgTutorial/Recipes/Antiquotes.thy	Fri May 17 07:29:51 2019 +0200
+++ b/ProgTutorial/Recipes/Antiquotes.thy	Fri May 17 10:38:01 2019 +0200
@@ -31,11 +31,10 @@
 
   We first describe the antiquotation \<open>ML_checked\<close> with the syntax:
  
-  @{text [display] "@{ML_checked \"a_piece_of_code\"}"}
+  @{text [display] \<open>@{ML_checked "a_piece_of_code"}\<close>}
 
   The code is checked by sending the ML-expression @{text [quotes] "val _ =
-  a_piece_of_code"} to the ML-compiler (i.e.~the function @{ML
-  "ML_Context.eval_source_in"} in Line 7 below). The complete code of the
+  a_piece_of_code"} to the ML-compiler (i.e.~the function @{ML \<open>ML_Context.eval_source_in\<close>} in Line 7 below). The complete code of the
   document antiquotation is as follows:
 
 \<close>
@@ -58,26 +57,26 @@
 
 
 text \<open>
-  The parser @{ML "(Scan.lift Args.name)"} in Line 7 parses a string, in this
+  The parser @{ML \<open>(Scan.lift Args.name)\<close>} in Line 7 parses a string, in this
   case the code, and then calls the function @{ML output_ml}. As mentioned
   before, the parsed code is sent to the ML-compiler in Line 4 using the
   function @{ML ml_val}, which constructs the appropriate ML-expression, and
-  using @{ML "eval_in" in ML_Context}, which calls the compiler.  If the code is
-  ``approved'' by the compiler, then the output function @{ML "output" in
+  using @{ML \<open>eval_in\<close> in ML_Context}, which calls the compiler.  If the code is
+  ``approved'' by the compiler, then the output function @{ML \<open>output\<close> in
   Document_Antiquotation} in the next line pretty prints the code. This function expects
   that the code is a list of (pretty)strings where each string correspond to a
-  line in the output. Therefore the use of @{ML "(space_explode \"\\n\" txt)"
+  line in the output. Therefore the use of @{ML \<open>(space_explode "\\n" txt)\<close>
   for txt} which produces such a list according to linebreaks.  There are a
   number of options for antiquotations that are observed by the function 
-  @{ML "output" in Document_Antiquotation} when printing the code (including \<open>[display]\<close> 
-  and \<open>[quotes]\<close>). The function @{ML "antiquotation_raw" in Thy_Output} in 
+  @{ML \<open>output\<close> in Document_Antiquotation} when printing the code (including \<open>[display]\<close> 
+  and \<open>[quotes]\<close>). The function @{ML \<open>antiquotation_raw\<close> in Thy_Output} in 
   Line 7 sets up the new document antiquotation.
 
   \begin{readmore}
   For more information about options of document antiquotations see \rsccite{sec:antiq}).
   \end{readmore}
 
-  Since we used the argument @{ML "Position.none"}, the compiler cannot give specific 
+  Since we used the argument @{ML \<open>Position.none\<close>}, the compiler cannot give specific 
   information about the line number, in case an error is detected. We 
   can improve the code above slightly by writing 
 \<close>
@@ -116,7 +115,7 @@
   going to implement the document antiquotation:
 
   
-  @{text [display] "@{ML_resp \"a_piece_of_code\" \"a_pattern\"}"}
+  @{text [display] \<open>@{ML_resp "a_piece_of_code" "a_pattern"}\<close>}
   
   To add some convenience and also to deal with large outputs, the user can
   give a partial specification by using ellipses. For example \<open>(\<dots>, \<dots>)\<close>
@@ -193,7 +192,7 @@
   the output (Lines 4 to 7) and the parser in the setup (Line 11). Now 
   you can write
  
-  @{text [display] "@{ML_resp [display] \"true andalso false\" \"false\"}"}
+  @{text [display] \<open>@{ML_resp [display] "true andalso false" "false"}\<close>}
 
   to obtain
 
@@ -201,7 +200,7 @@
 
   or 
 
-  @{text [display] "@{ML_resp [display] \"let val i = 3 in (i * i, \"foo\") end\" \"(9, \<dots>)\"}"}
+  @{text [display] \<open>@{ML_resp [display] "let val i = 3 in (i * i, "foo") end" "(9, \<dots>)"}\<close>}
   
   to obtain
 
diff -r be23597e81db -r f875a25aa72d ProgTutorial/Recipes/ExternalSolver.thy
--- a/ProgTutorial/Recipes/ExternalSolver.thy	Fri May 17 07:29:51 2019 +0200
+++ b/ProgTutorial/Recipes/ExternalSolver.thy	Fri May 17 10:38:01 2019 +0200
@@ -20,7 +20,7 @@
   For example, consider running an ordinary shell commands:
 
   @{ML_matchresult [display,gray] 
-    "Isabelle_System.bash_output \"echo Hello world!\"" "(\"Hello world!\\n\", 0)"}
+    \<open>Isabelle_System.bash_output "echo Hello world!"\<close> \<open>("Hello world!\n", 0)\<close>}
 
   Note that it works also fine with timeouts (see Recipe~\ref{rec:timeout}
   on Page~\pageref{rec:timeout}), i.e. external applications are killed
@@ -28,8 +28,8 @@
   one second:
 
   @{ML_matchresult_fake [display,gray] 
-    "Timeout.apply (Time.fromSeconds 1) Isabelle_System.bash_output \"sleep 30\"
-     handle TIMEOUT => (\"timeout\", ~1)" "(\"timeout\", ~1)"}
+    \<open>Timeout.apply (Time.fromSeconds 1) Isabelle_System.bash_output "sleep 30"
+     handle TIMEOUT => ("timeout", ~1)\<close> \<open>("timeout", ~1)\<close>}
 
   The function @{ML bash_output in Isabelle_System} can also be used for more reasonable
   applications, e.g. coupling external solvers with Isabelle. In that case,
@@ -46,7 +46,7 @@
 
   In Isabelle, this application may now be executed by
 
-  @{ML_matchresult_fake [display,gray] "Isabelle_System.bash_output \"$FOO\"" "\<dots>"}
+  @{ML_matchresult_fake [display,gray] \<open>Isabelle_System.bash_output "$FOO"\<close> \<open>\<dots>\<close>}
 \<close>
 
 
diff -r be23597e81db -r f875a25aa72d ProgTutorial/Recipes/Introspection.thy
--- a/ProgTutorial/Recipes/Introspection.thy	Fri May 17 07:29:51 2019 +0200
+++ b/ProgTutorial/Recipes/Introspection.thy	Fri May 17 10:38:01 2019 +0200
@@ -53,10 +53,10 @@
   established theorem. This can be done with
 
   @{ML_matchresult [display,gray]
-  "@{thm my_conjIa}
+  \<open>@{thm my_conjIa}
   |> Thm.proof_body_of
-  |> get_names"
-  "[\"Introspection.my_conjIa\"]"}
+  |> get_names\<close>
+  \<open>["Introspection.my_conjIa"]\<close>}
 \<close>
 text \<open>
   whereby \<open>Introspection\<close> refers to the theory name in which
@@ -68,13 +68,13 @@
   first level of the proof-tree, as follows.
 
   @{ML_matchresult_fake [display,gray]
-  "@{thm my_conjIa}
+  \<open>@{thm my_conjIa}
   |> Thm.proof_body_of
   |> get_pbodies
   |> map get_names
-  |> List.concat"
-  "[\"HOL.conjunct2\", \"HOL.conjunct1\", \"HOL.conjI\", \"Pure.protectD\", 
-  \"Pure.protectI\"]"}
+  |> List.concat\<close>
+  \<open>["HOL.conjunct2", "HOL.conjunct1", "HOL.conjI", "Pure.protectD", 
+  "Pure.protectI"]\<close>}
 \<close>
 text \<open>
   The theorems @{thm [source] protectD} and @{thm [source]
@@ -83,12 +83,12 @@
   count as a separate theorem, as you can see in the following code.
 
   @{ML_matchresult_fake [display,gray]
-  "@{thm my_conjIb}
+  \<open>@{thm my_conjIb}
   |> Thm.proof_body_of
   |> get_pbodies
   |> map get_names
-  |> List.concat"
-  "[\"Pure.protectD\", \"Pure.protectI\"]"}
+  |> List.concat\<close>
+  \<open>["Pure.protectD", "Pure.protectI"]\<close>}
 \<close>
 text \<open>
   Interestingly, but not surprisingly, the proof of @{thm [source]
@@ -97,14 +97,14 @@
   are returned for @{thm [source] my_conjIc}.
 
   @{ML_matchresult_fake [display,gray]
-  "@{thm my_conjIc}
+  \<open>@{thm my_conjIc}
   |> Thm.proof_body_of
   |> get_pbodies
   |> map get_names
-  |> List.concat"
-  "[\"HOL.implies_True_equals\", \"HOL.Eq_TrueI\", \"HOL.simp_thms_25\", \"HOL.eq_reflection\", 
-    \"HOL.conjunct2\", \"HOL.conjunct1\", \"HOL.TrueI\", \"Pure.protectD\",
-    \"Pure.protectI\"]"}
+  |> List.concat\<close>
+  \<open>["HOL.implies_True_equals", "HOL.Eq_TrueI", "HOL.simp_thms_25", "HOL.eq_reflection", 
+    "HOL.conjunct2", "HOL.conjunct1", "HOL.TrueI", "Pure.protectD",
+    "Pure.protectI"]\<close>}
 \<close>
 text \<open>
   Of course we can also descend into the second level of the tree 
@@ -113,16 +113,16 @@
   @{thm [source] conjunct1}, @{thm [source] conjunct2} and @{thm [source] conjI}.
 
   @{ML_matchresult_fake [display, gray]
-  "@{thm my_conjIa}
+  \<open>@{thm my_conjIa}
   |> Thm.proof_body_of
   |> get_pbodies
   |> map get_pbodies
   |> (map o map) get_names
   |> List.concat
   |> List.concat
-  |> duplicates (op =)"
-  "[\"\", \"Pure.protectD\",
- \"Pure.protectI\"]"}
+  |> duplicates (op =)\<close>
+  \<open>["", "Pure.protectD",
+ "Pure.protectI"]\<close>}
 \<close>
 
 
diff -r be23597e81db -r f875a25aa72d ProgTutorial/Recipes/Oracle.thy
--- a/ProgTutorial/Recipes/Oracle.thy	Fri May 17 07:29:51 2019 +0200
+++ b/ProgTutorial/Recipes/Oracle.thy	Fri May 17 10:38:01 2019 +0200
@@ -76,21 +76,18 @@
 text \<open>
   Here is the string representation of the term @{term "p = (q = p)"}:
 
-  @{ML_matchresult 
-    "translate @{term \"p = (q = p)\"}" 
-    "\" ( p <=> ( q <=> p ) ) \""}
+  @{ML_matchresult \<open>translate @{term "p = (q = p)"}\<close> 
+    \<open>" ( p <=> ( q <=> p ) ) "\<close>}
 
   Let us check, what the solver returns when given a tautology:
 
-  @{ML_matchresult 
-    "IffSolver.decide (translate @{term \"p = (q = p) = q\"})"
-    "true"}
+  @{ML_matchresult \<open>IffSolver.decide (translate @{term "p = (q = p) = q"})\<close>
+    \<open>true\<close>}
 
   And here is what it returns for a formula which is not valid:
 
-  @{ML_matchresult 
-    "IffSolver.decide (translate @{term \"p = (q = p)\"})" 
-    "false"}
+  @{ML_matchresult \<open>IffSolver.decide (translate @{term "p = (q = p)"})\<close> 
+    \<open>false\<close>}
 \<close>
 
 text \<open>
@@ -113,7 +110,7 @@
 text \<open>
   Here is what we get when applying the oracle:
 
-  @{ML_matchresult_fake "iff_oracle @{cprop \"p = (p::bool)\"}" "p = p"}
+  @{ML_matchresult_fake \<open>iff_oracle @{cprop "p = (p::bool)"}\<close> \<open>p = p\<close>}
 
   (FIXME: is there a better way to present the theorem?)
 
diff -r be23597e81db -r f875a25aa72d ProgTutorial/Recipes/Sat.thy
--- a/ProgTutorial/Recipes/Sat.thy	Fri May 17 07:29:51 2019 +0200
+++ b/ProgTutorial/Recipes/Sat.thy	Fri May 17 10:38:01 2019 +0200
@@ -33,7 +33,7 @@
 text \<open>
   then the resulting propositional formula @{ML pform} is 
   
-  @{ML [display] "Or (And (BoolVar 1, Not (BoolVar 1)), BoolVar 2)" in Prop_Logic} 
+  @{ML [display] \<open>Or (And (BoolVar 1, Not (BoolVar 1)), BoolVar 2)\<close> in Prop_Logic} 
   
 
   where indices are assigned for the variables 
@@ -43,8 +43,8 @@
   input table is empty (i.e.~@{ML Termtab.empty}) and the output table is
 
   @{ML_matchresult_fake [display,gray]
-  "Termtab.dest table"
-  "[(Free (\"A\", \"bool\"), 1), (Free (\"B\", \"bool\"), 2)]"}
+  \<open>Termtab.dest table\<close>
+  \<open>[(Free ("A", "bool"), 1), (Free ("B", "bool"), 2)]\<close>}
 
   An index is also produced whenever the translation
   function cannot find an appropriate propositional formula for a term. 
@@ -55,22 +55,22 @@
        Prop_Logic.prop_formula_of_term @{term "\<forall>x::nat. P x"}  Termtab.empty\<close>
 
 text \<open>
-  returns @{ML "BoolVar 1" in Prop_Logic} for  @{ML pform'} and the table 
+  returns @{ML \<open>BoolVar 1\<close> in Prop_Logic} for  @{ML pform'} and the table 
   @{ML table'} is:
 
   @{ML_matchresult_fake [display,gray]
-  "map (apfst (Syntax.string_of_term @{context})) (Termtab.dest table')"
-  "(\<forall>x. P x, 1)"}
+  \<open>map (apfst (Syntax.string_of_term @{context})) (Termtab.dest table')\<close>
+  \<open>(\<forall>x. P x, 1)\<close>}
   
   In the print out of the tabel, we used some pretty printing scaffolding 
   to see better which assignment the table contains.
  
   Having produced a propositional formula, you can now call the SAT solvers 
-  with the function @{ML "SAT_Solver.invoke_solver"}. For example
+  with the function @{ML \<open>SAT_Solver.invoke_solver\<close>}. For example
 
   @{ML_matchresult_fake [display,gray]
-  "SAT_Solver.invoke_solver \"minisat\" pform"
-  "SAT_Solver.SATISFIABLE assg"}
+  \<open>SAT_Solver.invoke_solver "minisat" pform\<close>
+  \<open>SAT_Solver.SATISFIABLE assg\<close>}
 \<close>
 
 text \<open>
@@ -78,12 +78,12 @@
   the returned function \<open>assg\<close>
 
   @{ML_matchresult [display,gray]
-"let
-  val SAT_Solver.SATISFIABLE assg = SAT_Solver.invoke_solver \"auto\" pform
+\<open>let
+  val SAT_Solver.SATISFIABLE assg = SAT_Solver.invoke_solver "auto" pform
 in 
   (assg 1, assg 2, assg 3)
-end"
-  "(NONE, SOME true, NONE)"}
+end\<close>
+  \<open>(NONE, SOME true, NONE)\<close>}
 
   we obtain a possible assignment for the variables \<open>A\<close> an \<open>B\<close>
   that makes the formula satisfiable. 
@@ -102,7 +102,7 @@
 done
 
 text \<open>
-  However, for proving anything more exciting using @{ML "sat_tac" in SAT} you 
+  However, for proving anything more exciting using @{ML \<open>sat_tac\<close> in SAT} you 
   have to use a SAT solver that can produce a proof. The internal 
   one is not usuable for this. 
 
diff -r be23597e81db -r f875a25aa72d ProgTutorial/Recipes/TimeLimit.thy
--- a/ProgTutorial/Recipes/TimeLimit.thy	Fri May 17 07:29:51 2019 +0200
+++ b/ProgTutorial/Recipes/TimeLimit.thy	Fri May 17 10:38:01 2019 +0200
@@ -21,25 +21,25 @@
 
   Now the call 
 
-  @{ML_matchresult_fake_both [display,gray] "ackermann (4, 12)" "\<dots>"}
+  @{ML_matchresult_fake_both [display,gray] \<open>ackermann (4, 12)\<close> \<open>\<dots>\<close>}
 
   takes a bit of time before it finishes. To avoid this, the call can be encapsulated 
   in a time limit of five seconds. For this you have to write
 
 @{ML_matchresult_fake_both [display,gray]
-"Timeout.apply (Time.fromSeconds 5) ackermann (4, 12) 
-  handle TIMEOUT => ~1"
-"~1"}
+\<open>Timeout.apply (Time.fromSeconds 5) ackermann (4, 12) 
+  handle TIMEOUT => ~1\<close>
+\<open>~1\<close>}
 
   where \<open>TimeOut\<close> is the exception raised when the time limit
   is reached.
 
-  Note that @{ML  "apply" in Timeout} is only meaningful when you use PolyML 5.2.1
+  Note that @{ML \<open>apply\<close> in Timeout} is only meaningful when you use PolyML 5.2.1
   or later, because this version of PolyML has the infrastructure for multithreaded 
-  programming on which @{ML "apply" in Timeout} relies.
+  programming on which @{ML \<open>apply\<close> in Timeout} relies.
 
 \begin{readmore}
-   The function @{ML "apply" in Timeout} is defined in the structure
+   The function @{ML \<open>apply\<close> in Timeout} is defined in the structure
   @{ML_structure Timeout} which can be found in the file 
   @{ML_file "Pure/concurrent/timeout.ML"}.
 \end{readmore}
diff -r be23597e81db -r f875a25aa72d ProgTutorial/Recipes/Timing.thy
--- a/ProgTutorial/Recipes/Timing.thy	Fri May 17 07:29:51 2019 +0200
+++ b/ProgTutorial/Recipes/Timing.thy	Fri May 17 10:38:01 2019 +0200
@@ -41,7 +41,7 @@
   tactics are lazy functions and you need to force them to run, otherwise the
   timing will be meaningless. The simplifier tactic, amongst others,  can be 
   forced to run by just applying the state to it. But ``fully'' lazy tactics,
-  such as @{ML "resolve_tac"}, need even more ``standing-on-ones-head'' to force
+  such as @{ML \<open>resolve_tac\<close>}, need even more ``standing-on-ones-head'' to force
   them to run. 
 
   The time between start and finish of the simplifier will be calculated 
diff -r be23597e81db -r f875a25aa72d ProgTutorial/Solutions.thy
--- a/ProgTutorial/Solutions.thy	Fri May 17 07:29:51 2019 +0200
+++ b/ProgTutorial/Solutions.thy	Fri May 17 10:38:01 2019 +0200
@@ -56,11 +56,11 @@
   as follows:
 
   @{ML_matchresult_fake [display,gray]
-  "@{prop \"\<forall>x y z. P x = P z\"}
+  \<open>@{prop "\<forall>x y z. P x = P z"}
   |> kill_trivial_quantifiers
   |> pretty_term @{context} 
-  |> pwriteln"
-  "\<forall>x z. P x = P z"}
+  |> pwriteln\<close>
+  \<open>\<forall>x z. P x = P z\<close>}
 \<close>
 
 
@@ -111,13 +111,13 @@
   normally return. For example:
 
   @{ML_matchresult [display,gray]
-"let
-  val input1 = (Symbol.explode \"foo bar\")
-  val input2 = (Symbol.explode \"foo (*test*) bar (*test*)\")
+\<open>let
+  val input1 = (Symbol.explode "foo bar")
+  val input2 = (Symbol.explode "foo (*test*) bar (*test*)")
 in
   (scan_all input1, scan_all input2)
-end"
-"(\"foo bar\", \"foo (**test**) bar (**test**)\")"}
+end\<close>
+\<open>("foo bar", "foo (**test**) bar (**test**)")\<close>}
 \<close>
 
 text \<open>\solution{ex:contextfree}\<close>
@@ -331,8 +331,8 @@
   This function generates for example:
 
   @{ML_matchresult_fake [display,gray] 
-  "pwriteln (pretty_term @{context} (term_tree 2))" 
-  "(1 + 2) + (3 + 4)"} 
+  \<open>pwriteln (pretty_term @{context} (term_tree 2))\<close> 
+  \<open>(1 + 2) + (3 + 4)\<close>} 
 
   The next function constructs a goal of the form \<open>P \<dots>\<close> with a term 
   produced by @{ML term_tree} filled in.
@@ -344,7 +344,7 @@
   Note that the goal needs to be wrapped in a @{term "Trueprop"}. Next we define
   two tactics, \<open>c_tac\<close> and \<open>s_tac\<close>, for the conversion and simproc,
   respectively. The idea is to first apply the conversion (respectively simproc) and 
-  then prove the remaining goal using @{ML "cheat_tac" in Skip_Proof}.
+  then prove the remaining goal using @{ML \<open>cheat_tac\<close> in Skip_Proof}.
 \<close>
 
 ML Skip_Proof.cheat_tac
diff -r be23597e81db -r f875a25aa72d ProgTutorial/Tactical.thy
--- a/ProgTutorial/Tactical.thy	Fri May 17 07:29:51 2019 +0200
+++ b/ProgTutorial/Tactical.thy	Fri May 17 10:38:01 2019 +0200
@@ -48,17 +48,17 @@
   This proof translates to the following ML-code.
   
 @{ML_matchresult_fake [display,gray]
-"let
+\<open>let
   val ctxt = @{context}
-  val goal = @{prop \"P \<or> Q \<Longrightarrow> Q \<or> P\"}
+  val goal = @{prop "P \<or> Q \<Longrightarrow> Q \<or> P"}
 in
-  Goal.prove ctxt [\"P\", \"Q\"] [] goal 
+  Goal.prove ctxt ["P", "Q"] [] goal 
    (fn _ =>  eresolve_tac @{context} [@{thm disjE}] 1
              THEN resolve_tac @{context} [@{thm disjI2}] 1
              THEN assume_tac @{context} 1
              THEN resolve_tac @{context} [@{thm disjI1}] 1
              THEN assume_tac @{context} 1)
-end" "?P \<or> ?Q \<Longrightarrow> ?Q \<or> ?P"}
+end\<close> \<open>?P \<or> ?Q \<Longrightarrow> ?Q \<or> ?P\<close>}
   
   To start the proof, the function @{ML_ind prove in Goal} sets up a goal
   state for proving the goal @{prop "P \<or> Q \<Longrightarrow> Q \<or> P"}. We can give this
@@ -764,16 +764,16 @@
   The function @{ML_ind RS in Drule}, for example, does this.
   
   @{ML_matchresult_fake [display,gray]
-  "@{thm disjI1} RS @{thm conjI}" "\<lbrakk>?P1; ?Q\<rbrakk> \<Longrightarrow> (?P1 \<or> ?Q1) \<and> ?Q"}
+  \<open>@{thm disjI1} RS @{thm conjI}\<close> \<open>\<lbrakk>?P1; ?Q\<rbrakk> \<Longrightarrow> (?P1 \<or> ?Q1) \<and> ?Q\<close>}
 
   In this example it instantiates the first premise of the \<open>conjI\<close>-theorem 
   with the theorem \<open>disjI1\<close>. If the instantiation is impossible, as in the 
   case of
 
   @{ML_matchresult_fake_both [display,gray]
-  "@{thm conjI} RS @{thm mp}" 
-"*** Exception- THM (\"RSN: no unifiers\", 1, 
-[\"\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q\", \"\<lbrakk>?P \<longrightarrow> ?Q; ?P\<rbrakk> \<Longrightarrow> ?Q\"]) raised"}
+  \<open>@{thm conjI} RS @{thm mp}\<close> 
+\<open>*** Exception- THM ("RSN: no unifiers", 1, 
+["\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q", "\<lbrakk>?P \<longrightarrow> ?Q; ?P\<rbrakk> \<Longrightarrow> ?Q"]) raised\<close>}
 
   then the function raises an exception. The function @{ML_ind  RSN in Drule} 
   is similar to @{ML RS}, but takes an additional number as argument. This 
@@ -783,8 +783,8 @@
   the function @{ML_ind MRS in Drule}:
 
   @{ML_matchresult_fake [display,gray]
-  "[@{thm disjI1}, @{thm disjI2}] MRS @{thm conjI}" 
-  "\<lbrakk>?P2; ?Q1\<rbrakk> \<Longrightarrow> (?P2 \<or> ?Q2) \<and> (?P1 \<or> ?Q1)"}
+  \<open>[@{thm disjI1}, @{thm disjI2}] MRS @{thm conjI}\<close> 
+  \<open>\<lbrakk>?P2; ?Q1\<rbrakk> \<Longrightarrow> (?P2 \<or> ?Q2) \<and> (?P1 \<or> ?Q1)\<close>}
 
   If you need to instantiate lists of theorems, you can use the
   functions @{ML_ind RL in Drule} and @{ML_ind OF in Drule}. For 
@@ -792,16 +792,16 @@
   instantiated with every theorem in the first.
 
   @{ML_matchresult_fake [display,gray]
-"let
+\<open>let
   val list1 = [@{thm impI}, @{thm disjI2}]
   val list2 = [@{thm conjI}, @{thm disjI1}]
 in
   list1 RL list2
-end" 
-"[\<lbrakk>?P1 \<Longrightarrow> ?Q1; ?Q\<rbrakk> \<Longrightarrow> (?P1 \<longrightarrow> ?Q1) \<and> ?Q, 
+end\<close> 
+\<open>[\<lbrakk>?P1 \<Longrightarrow> ?Q1; ?Q\<rbrakk> \<Longrightarrow> (?P1 \<longrightarrow> ?Q1) \<and> ?Q, 
  \<lbrakk>?Q1; ?Q\<rbrakk> \<Longrightarrow> (?P1 \<or> ?Q1) \<and> ?Q,
  (?P1 \<Longrightarrow> ?Q1) \<Longrightarrow> (?P1 \<longrightarrow> ?Q1) \<or> ?Q, 
- ?Q1 \<Longrightarrow> (?P1 \<or> ?Q1) \<or> ?Q]"}
+ ?Q1 \<Longrightarrow> (?P1 \<or> ?Q1) \<or> ?Q]\<close>}
 
   \begin{readmore}
   The combinators for instantiating theorems with other theorems are 
@@ -981,7 +981,7 @@
   There is even another way of implementing this tactic: in automatic proof
   procedures (in contrast to tactics that might be called by the user) there
   are often long lists of tactics that are applied to the first
-  subgoal. Instead of writing the code above and then calling @{ML "foo_tac'' @{context} 1"}, 
+  subgoal. Instead of writing the code above and then calling @{ML \<open>foo_tac'' @{context} 1\<close>}, 
   you can also just write
 \<close>
 
@@ -1097,7 +1097,7 @@
   convention therefore, tactics visible to the user should either change
   something or fail.
 
-  To comply with this convention, we could simply delete the @{ML "K all_tac"}
+  To comply with this convention, we could simply delete the @{ML \<open>K all_tac\<close>}
   in @{ML select_tac'} or delete @{ML TRY} from @{ML select_tac''}. But for
   the sake of argument, let us suppose that this deletion is \emph{not} an
   option. In such cases, you can use the combinator @{ML_ind CHANGED in
@@ -1459,10 +1459,10 @@
   empty simpset, i.e., @{ML_ind empty_ss in Raw_Simplifier}
   
   @{ML_matchresult_fake [display,gray]
-  "print_ss @{context} empty_ss"
-"Simplification rules:
+  \<open>print_ss @{context} empty_ss\<close>
+\<open>Simplification rules:
 Congruences rules:
-Simproc patterns:"}
+Simproc patterns:\<close>}
 
   you can see it contains nothing. This simpset is usually not useful, except as a 
   building block to build bigger simpsets. For example you can add to @{ML empty_ss} 
@@ -1475,11 +1475,11 @@
   Printing then out the components of the simpset gives:
 
   @{ML_matchresult_fake [display,gray]
-  "print_ss @{context} (Raw_Simplifier.simpset_of ss1)"
-"Simplification rules:
+  \<open>print_ss @{context} (Raw_Simplifier.simpset_of ss1)\<close>
+\<open>Simplification rules:
   ??.unknown: A - B \<inter> C \<equiv> A - B \<union> (A - C)
 Congruences rules:
-Simproc patterns:"}
+Simproc patterns:\<close>}
 
   \footnote{\bf FIXME: Why does it print out ??.unknown}
 
@@ -1492,13 +1492,13 @@
   gives
 
   @{ML_matchresult_fake [display,gray]
-  "print_ss @{context} (Raw_Simplifier.simpset_of ss2)"
-"Simplification rules:
+  \<open>print_ss @{context} (Raw_Simplifier.simpset_of ss2)\<close>
+\<open>Simplification rules:
   ??.unknown: A - B \<inter> C \<equiv> A - B \<union> (A - C)
 Congruences rules:
   Complete_Lattices.Inf_class.INFIMUM: 
     \<lbrakk>A1 = B1; \<And>x. x \<in> B1 =simp=> C1 x = D1 x\<rbrakk> \<Longrightarrow> INFIMUM A1 C1 \<equiv> INFIMUM B1 D1
-Simproc patterns:"}
+Simproc patterns:\<close>}
 
   Notice that we had to add these lemmas as meta-equations. The @{ML empty_ss} 
   expects this form of the simplification and congruence rules. This is
@@ -1509,10 +1509,10 @@
   HOL_basic_ss in Simpdata}. While printing out the components of this simpset
 
   @{ML_matchresult_fake [display,gray]
-  "print_ss @{context} HOL_basic_ss"
-"Simplification rules:
+  \<open>print_ss @{context} HOL_basic_ss\<close>
+\<open>Simplification rules:
 Congruences rules:
-Simproc patterns:"}
+Simproc patterns:\<close>}
 
   also produces ``nothing'', the printout is somewhat misleading. In fact
   the @{ML HOL_basic_ss} is setup so that it can solve goals of the
@@ -1543,8 +1543,8 @@
   connectives in HOL. 
 
   @{ML_matchresult_fake [display,gray]
-  "print_ss @{context} HOL_ss"
-"Simplification rules:
+  \<open>print_ss @{context} HOL_ss\<close>
+\<open>Simplification rules:
   Pure.triv_forall_equality: (\<And>x. PROP V) \<equiv> PROP V
   HOL.the_eq_trivial: THE x. x = y \<equiv> y
   HOL.the_sym_eq_trivial: THE ya. y = ya \<equiv> y
@@ -1554,7 +1554,7 @@
     \<Longrightarrow> (PROP P =simp=> PROP Q) \<equiv> (PROP P' =simp=> PROP Q')
   op -->: \<lbrakk>P \<equiv> P'; P' \<Longrightarrow> Q \<equiv> Q'\<rbrakk> \<Longrightarrow> P \<longrightarrow> Q \<equiv> P' \<longrightarrow> Q'
 Simproc patterns:
-  \<dots>"}
+  \<dots>\<close>}
 
   \begin{readmore}
   The simplifier for HOL is set up in @{ML_file "HOL/Tools/simpdata.ML"}.
@@ -1755,7 +1755,7 @@
 
   (FIXME: what are @{ML mksimps_pairs}; used in Nominal.thy)
 
-  (FIXME: explain @{ML simplify} and @{ML "Simplifier.rewrite_rule"} etc.)
+  (FIXME: explain @{ML simplify} and @{ML \<open>Simplifier.rewrite_rule\<close>} etc.)
 
 \<close>
 
@@ -2065,29 +2065,29 @@
   instance of the (meta)reflexivity theorem. For example:
 
   @{ML_matchresult_fake [display,gray]
-  "Conv.all_conv @{cterm \"Foo \<or> Bar\"}"
-  "Foo \<or> Bar \<equiv> Foo \<or> Bar"}
+  \<open>Conv.all_conv @{cterm "Foo \<or> Bar"}\<close>
+  \<open>Foo \<or> Bar \<equiv> Foo \<or> Bar\<close>}
 
   Another simple conversion is @{ML_ind  no_conv in Conv} which always raises the 
   exception @{ML CTERM}.
 
   @{ML_matchresult_fake [display,gray]
-  "Conv.no_conv @{cterm True}" 
-  "*** Exception- CTERM (\"no conversion\", []) raised"}
+  \<open>Conv.no_conv @{cterm True}\<close> 
+  \<open>*** Exception- CTERM ("no conversion", []) raised\<close>}
 
   A more interesting conversion is the function @{ML_ind  beta_conversion in Thm}: it 
   produces a meta-equation between a term and its beta-normal form. For example
 
   @{ML_matchresult_fake [display,gray]
-  "let
-  val add = @{cterm \"\<lambda>x y. x + (y::nat)\"}
-  val two = @{cterm \"2::nat\"}
-  val ten = @{cterm \"10::nat\"}
+  \<open>let
+  val add = @{cterm "\<lambda>x y. x + (y::nat)"}
+  val two = @{cterm "2::nat"}
+  val ten = @{cterm "10::nat"}
   val ctrm = Thm.apply (Thm.apply add two) ten
 in
   Thm.beta_conversion true ctrm
-end"
-  "((\<lambda>x y. x + y) 2) 10 \<equiv> 2 + 10"}
+end\<close>
+  \<open>((\<lambda>x y. x + y) 2) 10 \<equiv> 2 + 10\<close>}
 
   If you run this example, you will notice that the actual response is the 
   seemingly nonsensical @{term
@@ -2097,25 +2097,25 @@
   we obtain the expected result.
 
   @{ML_matchresult [display,gray]
-"let
-  val add = @{cterm \"\<lambda>x y. x + (y::nat)\"}
-  val two = @{cterm \"2::nat\"}
-  val ten = @{cterm \"10::nat\"}
+\<open>let
+  val add = @{cterm "\<lambda>x y. x + (y::nat)"}
+  val two = @{cterm "2::nat"}
+  val ten = @{cterm "10::nat"}
   val ctrm = Thm.apply (Thm.apply add two) ten
 in
   Thm.prop_of (Thm.beta_conversion true ctrm)
-end"
-"Const (\"Pure.eq\",_) $ 
-  (Abs (\"x\",_,Abs (\"y\",_,_)) $_$_) $ 
-    (Const (\"Groups.plus_class.plus\",_) $ _ $ _)"} 
+end\<close>
+\<open>Const ("Pure.eq",_) $ 
+  (Abs ("x",_,Abs ("y",_,_)) $_$_) $ 
+    (Const ("Groups.plus_class.plus",_) $ _ $ _)\<close>} 
 
 or in the pretty-printed form
 
   @{ML_matchresult_fake [display,gray]
-"let
-   val add = @{cterm \"\<lambda>x y. x + (y::nat)\"}
-   val two = @{cterm \"2::nat\"}
-   val ten = @{cterm \"10::nat\"}
+\<open>let
+   val add = @{cterm "\<lambda>x y. x + (y::nat)"}
+   val two = @{cterm "2::nat"}
+   val ten = @{cterm "10::nat"}
    val ctrm = Thm.apply (Thm.apply add two) ten
    val ctxt = @{context}
      |> Config.put eta_contract false 
@@ -2124,8 +2124,8 @@
   Thm.prop_of (Thm.beta_conversion true ctrm)
   |> pretty_term ctxt
   |> pwriteln
-end"
-"(\<lambda>x y. x + y) 2 10 \<equiv> 2 + 10"}
+end\<close>
+\<open>(\<lambda>x y. x + y) 2 10 \<equiv> 2 + 10\<close>}
 
   The argument @{ML true} in @{ML beta_conversion in Thm} indicates that 
   the right-hand side should be fully beta-normalised. If instead 
@@ -2147,12 +2147,12 @@
   to @{term "Foo \<longrightarrow> Bar"}. The code is as follows.
 
   @{ML_matchresult_fake [display,gray]
-"let 
-  val ctrm = @{cterm \"True \<and> (Foo \<longrightarrow> Bar)\"}
+\<open>let 
+  val ctrm = @{cterm "True \<and> (Foo \<longrightarrow> Bar)"}
 in
   Conv.rewr_conv @{thm true_conj1} ctrm
-end"
-  "True \<and> (Foo \<longrightarrow> Bar) \<equiv> Foo \<longrightarrow> Bar"}
+end\<close>
+  \<open>True \<and> (Foo \<longrightarrow> Bar) \<equiv> Foo \<longrightarrow> Bar\<close>}
 
   Note, however, that the function @{ML_ind  rewr_conv in Conv} only rewrites the 
   outer-most level of the @{ML_type cterm}. If the given @{ML_type cterm} does not match 
@@ -2166,14 +2166,14 @@
   which applies one conversion after another. For example
 
   @{ML_matchresult_fake [display,gray]
-"let
+\<open>let
   val conv1 = Thm.beta_conversion false
   val conv2 = Conv.rewr_conv @{thm true_conj1}
-  val ctrm = Thm.apply @{cterm \"\<lambda>x. x \<and> False\"} @{cterm \"True\"}
+  val ctrm = Thm.apply @{cterm "\<lambda>x. x \<and> False"} @{cterm "True"}
 in
   (conv1 then_conv conv2) ctrm
-end"
-  "(\<lambda>x. x \<and> False) True \<equiv> False"}
+end\<close>
+  \<open>(\<lambda>x. x \<and> False) True \<equiv> False\<close>}
 
   where we first beta-reduce the term and then rewrite according to
   @{thm [source] true_conj1}. (When running this example recall the 
@@ -2183,14 +2183,14 @@
   first one, and if it does not apply, tries the second. For example 
 
   @{ML_matchresult_fake [display,gray]
-"let
+\<open>let
   val conv = Conv.rewr_conv @{thm true_conj1} else_conv Conv.all_conv
-  val ctrm1 = @{cterm \"True \<and> Q\"}
-  val ctrm2 = @{cterm \"P \<or> (True \<and> Q)\"}
+  val ctrm1 = @{cterm "True \<and> Q"}
+  val ctrm2 = @{cterm "P \<or> (True \<and> Q)"}
 in
   (conv ctrm1, conv ctrm2)
-end"
-"(True \<and> Q \<equiv> Q, P \<or> True \<and> Q \<equiv> P \<or> True \<and> Q)"}
+end\<close>
+\<open>(True \<and> Q \<equiv> Q, P \<or> True \<and> Q \<equiv> P \<or> True \<and> Q)\<close>}
 
   Here the conversion @{thm [source] true_conj1} only applies
   in the first case, but fails in the second. The whole conversion
@@ -2200,13 +2200,13 @@
   For example
   
   @{ML_matchresult_fake [display,gray]
-"let
+\<open>let
   val conv = Conv.try_conv (Conv.rewr_conv @{thm true_conj1})
-  val ctrm = @{cterm \"True \<or> P\"}
+  val ctrm = @{cterm "True \<or> P"}
 in
   conv ctrm
-end"
-  "True \<or> P \<equiv> True \<or> P"}
+end\<close>
+  \<open>True \<or> P \<equiv> True \<or> P\<close>}
 
   Rewriting with more than one theorem can be done using the function 
   @{ML_ind rewrs_conv in Conv} from the structure @{ML_structure Conv}.
@@ -2221,13 +2221,13 @@
   For example
 
   @{ML_matchresult_fake [display,gray]
-"let 
+\<open>let 
   val conv = Conv.arg_conv (Conv.rewr_conv @{thm true_conj1})
-  val ctrm = @{cterm \"P \<or> (True \<and> Q)\"}
+  val ctrm = @{cterm "P \<or> (True \<and> Q)"}
 in
   conv ctrm
-end"
-"P \<or> (True \<and> Q) \<equiv> P \<or> Q"}
+end\<close>
+\<open>P \<or> (True \<and> Q) \<equiv> P \<or> Q\<close>}
 
   The reason for this behaviour is that \<open>(op \<or>)\<close> expects two
   arguments.  Therefore the term must be of the form \<open>(Const \<dots> $ t1) $ t2\<close>. The
@@ -2239,13 +2239,13 @@
   abstraction. For example:
 
   @{ML_matchresult_fake [display,gray]
-"let 
+\<open>let 
   val conv = Conv.rewr_conv @{thm true_conj1} 
-  val ctrm = @{cterm \"\<lambda>P. True \<and> (P \<and> Foo)\"}
+  val ctrm = @{cterm "\<lambda>P. True \<and> (P \<and> Foo)"}
 in
   Conv.abs_conv (K conv) @{context} ctrm
-end"
-  "\<lambda>P. True \<and> (P \<and> Foo) \<equiv> \<lambda>P. P \<and> Foo"}
+end\<close>
+  \<open>\<lambda>P. True \<and> (P \<and> Foo) \<equiv> \<lambda>P. P \<and> Foo\<close>}
   
   Note that this conversion needs a context as an argument. We also give the
   conversion as \<open>(K conv)\<close>, which is a function that ignores its
@@ -2280,13 +2280,13 @@
   conversion in action, consider the following example:
 
 @{ML_matchresult_fake [display,gray]
-"let
+\<open>let
   val conv = true_conj1_conv @{context}
-  val ctrm = @{cterm \"distinct [1::nat, x] \<longrightarrow> True \<and> 1 \<noteq> x\"}
+  val ctrm = @{cterm "distinct [1::nat, x] \<longrightarrow> True \<and> 1 \<noteq> x"}
 in
   conv ctrm
-end"
-  "distinct [1, x] \<longrightarrow> True \<and> 1 \<noteq> x \<equiv> distinct [1, x] \<longrightarrow> 1 \<noteq> x"}
+end\<close>
+  \<open>distinct [1, x] \<longrightarrow> True \<and> 1 \<noteq> x \<equiv> distinct [1, x] \<longrightarrow> 1 \<noteq> x\<close>}
 \<close>
 
 text \<open>
@@ -2323,17 +2323,17 @@
   two results are calculated. 
 
   @{ML_matchresult_fake [display, gray]
-  "let
+  \<open>let
   val ctxt = @{context}
   val conv = Conv.try_conv (Conv.rewrs_conv @{thms conj_assoc})
   val conv_top = Conv.top_conv (K conv) ctxt
   val conv_bot = Conv.bottom_conv (K conv) ctxt
-  val ctrm = @{cterm \"(a \<and> (b \<and> c)) \<and> d\"}
+  val ctrm = @{cterm "(a \<and> (b \<and> c)) \<and> d"}
 in
   (conv_top ctrm, conv_bot ctrm)
-end"
-  "(\"(a \<and> (b \<and> c)) \<and> d \<equiv> a \<and> (b \<and> (c \<and> d))\",
- \"(a \<and> (b \<and> c)) \<and> d \<equiv> (a \<and> b) \<and> (c \<and> d)\")"}
+end\<close>
+  \<open>("(a \<and> (b \<and> c)) \<and> d \<equiv> a \<and> (b \<and> (c \<and> d))",
+ "(a \<and> (b \<and> c)) \<and> d \<equiv> (a \<and> b) \<and> (c \<and> d)")\<close>}
 
   To see how much control you have over rewriting with conversions, let us 
   make the task a bit more complicated by rewriting according to the rule
@@ -2359,14 +2359,14 @@
 
 
   @{ML_matchresult_fake [display,gray]
-"let
-  val ctrm = @{cterm \"if P (True \<and> 1 \<noteq> (2::nat)) 
-                        then True \<and> True else True \<and> False\"}
+\<open>let
+  val ctrm = @{cterm "if P (True \<and> 1 \<noteq> (2::nat)) 
+                        then True \<and> True else True \<and> False"}
 in
   if_true1_conv @{context} ctrm
-end"
-"if P (True \<and> 1 \<noteq> 2) then True \<and> True else True \<and> False 
-\<equiv> if P (1 \<noteq> 2) then True \<and> True else True \<and> False"}
+end\<close>
+\<open>if P (True \<and> 1 \<noteq> 2) then True \<and> True else True \<and> False 
+\<equiv> if P (1 \<noteq> 2) then True \<and> True else True \<and> False\<close>}
 \<close>
 
 text \<open>
@@ -2383,13 +2383,13 @@
   new theorem as follows
 
   @{ML_matchresult_fake [display,gray]
-"let
+\<open>let
   val conv = Conv.fconv_rule (true_conj1_conv @{context}) 
   val thm = @{thm foo_test}
 in
   conv thm
-end" 
-  "?P \<or> \<not> ?P"}
+end\<close> 
+  \<open>?P \<or> \<not> ?P\<close>}
 
   Finally, Isabelle provides function @{ML_ind CONVERSION in Tactical} 
   for turning conversions into tactics. This needs some predefined conversion 
@@ -2420,7 +2420,7 @@
           Conv.concl_conv ~1 (true_conj1_conv ctxt))) ctxt)\<close>
 
 text \<open>
-  We call the conversions with the argument @{ML "~1"}. By this we 
+  We call the conversions with the argument @{ML \<open>~1\<close>}. By this we 
   analyse all parameters, all premises and the conclusion of a goal
   state. If we call @{ML concl_conv in Conv} with 
   a non-negative number, say \<open>n\<close>, then this conversions will 
@@ -2466,8 +2466,8 @@
   left-hand side in the right-hand side.
 
   @{ML_matchresult_fake [display,gray]
-  "Drule.abs_def @{thm id1_def}"
-  "id1 \<equiv> \<lambda>x. x"}
+  \<open>Drule.abs_def @{thm id1_def}\<close>
+  \<open>id1 \<equiv> \<lambda>x. x\<close>}
 
   Unfortunately, Isabelle has no built-in function that transforms the
   theorems in the other direction. We can implement one using
@@ -2514,8 +2514,8 @@
   produce meta-variables for the theorem.  An example is as follows.
 
   @{ML_matchresult_fake [display, gray]
-  "unabs_def @{context} @{thm id2_def}"
-  "id2 ?x1 \<equiv> ?x1"}
+  \<open>unabs_def @{context} @{thm id2_def}\<close>
+  \<open>id2 ?x1 \<equiv> ?x1\<close>}
 \<close>
 
 text \<open>