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