
diff -r 6e2479089226 -r cecd7a941885 ProgTutorial/First_Steps.thy
--- a/ProgTutorial/First_Steps.thy	Tue May 14 16:59:53 2019 +0200
+++ b/ProgTutorial/First_Steps.thy	Tue May 14 17:10:47 2019 +0200
@@ -2,11 +2,11 @@
 imports Base
 begin
                                                   
-chapter {* First Steps\label{chp:firststeps} *}
+chapter \<open>First Steps\label{chp:firststeps}\<close>
 
 
 
-text {*
+text \<open>
   \begin{flushright}
   {\em ``The most effective debugging tool is still careful thought,\\ 
   coupled with judiciously placed print statements.''} \\[1ex]
@@ -29,20 +29,20 @@
 
   We also generally assume you are working with the logic HOL. The examples
   that will be given might need to be adapted if you work in a different logic.
-*}
+\<close>
 
-section {* Including ML-Code\label{sec:include} *}
+section \<open>Including ML-Code\label{sec:include}\<close>
 
-text {*
+text \<open>
   The easiest and quickest way to include code in a theory is by using the
   \isacommand{ML}-command. For example:
 
   \begin{isabelle}
   \begin{graybox}
-  \isacommand{ML}~@{text "\<verbopen>"}\isanewline
+  \isacommand{ML}~\<open>\<verbopen>\<close>\isanewline
   \hspace{5mm}@{ML "3 + 4"}\isanewline
-  @{text "\<verbclose>"}\isanewline
-  @{text "> 7"}\smallskip
+  \<open>\<verbclose>\<close>\isanewline
+  \<open>> 7\<close>\smallskip
   \end{graybox}
   \end{isabelle}
 
@@ -52,8 +52,7 @@
   Jedit GUI, then you just have to hover the cursor over the code 
   and you see the evaluated result in the ``Output'' window.
 
-  As mentioned in the Introduction, we will drop the \isacommand{ML}~@{text
-  "\<verbopen> \<dots> \<verbclose>"} scaffolding whenever we show code. The lines
+  As mentioned in the Introduction, we will drop the \isacommand{ML}~\<open>\<verbopen> \<dots> \<verbclose>\<close> scaffolding whenever we show code. The lines
   prefixed with @{text [quotes] ">"} are not part of the code, rather they
   indicate what the response is when the code is evaluated.  There are also
   the commands \isacommand{ML\_val} and \isacommand{ML\_prf} for including
@@ -63,9 +62,9 @@
 
   \begin{quote}
   \begin{isabelle}
-  \isacommand{lemma}~@{text "test:"}\isanewline
+  \isacommand{lemma}~\<open>test:\<close>\isanewline
   \isacommand{shows}~@{text [quotes] "True"}\isanewline
-  \isacommand{ML\_prf}~@{text "\<verbopen>"}~@{ML "writeln \"Trivial!\""}~@{text "\<verbclose>"}\isanewline
+  \isacommand{ML\_prf}~\<open>\<verbopen>\<close>~@{ML "writeln \"Trivial!\""}~\<open>\<verbclose>\<close>\isanewline
   \isacommand{oops}
   \end{isabelle}
   \end{quote}
@@ -84,15 +83,15 @@
   \isacommand{imports} Main\\
   \isacommand{begin}\\
   \ldots\\
-  \isacommand{ML\_file}~@{text "\"file_to_be_included.ML\""}\\
+  \isacommand{ML\_file}~\<open>"file_to_be_included.ML"\<close>\\
   \ldots
   \end{tabular}
   \end{quote}
-*}
+\<close>
 
-section {* Printing and Debugging\label{sec:printing} *}
+section \<open>Printing and Debugging\label{sec:printing}\<close>
 
-text {*
+text \<open>
   During development you might find it necessary to inspect data in your
   code. This can be done in a ``quick-and-dirty'' fashion using the function
   @{ML_ind writeln in Output}. For example
@@ -103,11 +102,11 @@
   This function expects a string as argument. If you develop under
   PolyML, then there is a convenient, though again ``quick-and-dirty'', method
   for converting values into strings, namely the antiquotation 
-  @{text "@{make_string}"}:
+  \<open>@{make_string}\<close>:
 
   @{ML_response_fake [display,gray] "writeln (@{make_string} 1)" "\"1\""} 
 
-  However, @{text "@{make_string}"} only works if the type of what
+  However, \<open>@{make_string}\<close> only works if the type of what
   is converted is monomorphic and not a function. 
 
   You can print out error messages with the function @{ML_ind error in Library}; 
@@ -118,12 +117,12 @@
 "*** foo
 ***"}
 
-  This function raises the exception @{text ERROR}, which will then 
+  This function raises the exception \<open>ERROR\<close>, which will then 
   be displayed by the infrastructure indicating that it is an error by
   painting the output red. Note that this exception is meant 
   for ``user-level'' error messages seen by the ``end-user''. 
   For messages where you want to indicate a genuine program error
-  use the exception @{text Fail}. 
+  use the exception \<open>Fail\<close>. 
 
   Most often you want to inspect contents of Isabelle's basic data structures,
   namely @{ML_type term}, @{ML_type typ}, @{ML_type cterm}, @{ML_type ctyp}
@@ -132,12 +131,12 @@
   we just use the functions @{ML_ind writeln in Pretty}  from the structure
   @{ML_struct Pretty} and @{ML_ind pretty_term in Syntax} from the structure
   @{ML_struct Syntax}. For more convenience, we bind them to the toplevel.
-*}
+\<close>
 
-ML %grayML{*val pretty_term = Syntax.pretty_term
-val pwriteln = Pretty.writeln*}
+ML %grayML\<open>val pretty_term = Syntax.pretty_term
+val pwriteln = Pretty.writeln\<close>
 
-text {*
+text \<open>
   They can be used as follows
 
   @{ML_response_fake [display,gray]
@@ -147,27 +146,27 @@
   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} 
   to separate them.
-*} 
+\<close> 
 
-ML %grayML{*fun pretty_terms ctxt trms =  
-  Pretty.block (Pretty.commas (map (pretty_term ctxt) trms))*}
+ML %grayML\<open>fun pretty_terms ctxt trms =  
+  Pretty.block (Pretty.commas (map (pretty_term ctxt) trms))\<close>
 
-text {*
+text \<open>
   To print out terms together with their typing information,
   set the configuration value
   @{ML_ind show_types in Syntax} to @{ML true}.
-*}
+\<close>
 
-ML %grayML{*val show_types_ctxt = Config.put show_types true @{context}*}
+ML %grayML\<open>val show_types_ctxt = Config.put show_types true @{context}\<close>
 
-text {*
+text \<open>
   Now by using this context @{ML pretty_term} prints out
 
   @{ML_response_fake [display, gray]
   "pwriteln (pretty_term show_types_ctxt @{term \"(1::nat, x)\"})"
   "(1::nat, x::'a)"}
 
-  where @{text 1} and @{text x} are displayed with their inferred types.
+  where \<open>1\<close> and \<open>x\<close> are displayed with their inferred types.
   Other configuration values that influence
   printing of terms include 
 
@@ -178,34 +177,34 @@
   \end{itemize}
 
   A @{ML_type cterm} can be printed with the following function.
-*}
+\<close>
 
-ML %grayML %grayML{*fun pretty_cterm ctxt ctrm =  
-  pretty_term ctxt (Thm.term_of ctrm)*}
+ML %grayML %grayML\<open>fun pretty_cterm ctxt ctrm =  
+  pretty_term ctxt (Thm.term_of ctrm)\<close>
 
-text {*
+text \<open>
   Here the function @{ML_ind term_of in Thm} extracts the @{ML_type
   term} from a @{ML_type cterm}.  More than one @{ML_type cterm}s can be
   printed again with @{ML commas in Pretty}.
-*} 
+\<close> 
 
-ML %grayML{*fun pretty_cterms ctxt ctrms =  
-  Pretty.block (Pretty.commas (map (pretty_cterm ctxt) ctrms))*}
+ML %grayML\<open>fun pretty_cterms ctxt ctrms =  
+  Pretty.block (Pretty.commas (map (pretty_cterm ctxt) ctrms))\<close>
 
-text {*
+text \<open>
   The easiest way to get the string of a theorem is to transform it
   into a @{ML_type term} using the function @{ML_ind prop_of in Thm}. 
-*}
+\<close>
 
-ML %grayML{*fun pretty_thm ctxt thm =
-  pretty_term ctxt (Thm.prop_of thm)*}
+ML %grayML\<open>fun pretty_thm ctxt thm =
+  pretty_term ctxt (Thm.prop_of thm)\<close>
 
-text {*
-  Theorems include schematic variables, such as @{text "?P"}, 
-  @{text "?Q"} and so on. They are instantiated by Isabelle when a theorem is applied.
+text \<open>
+  Theorems include schematic variables, such as \<open>?P\<close>, 
+  \<open>?Q\<close> and so on. They are instantiated by Isabelle when a theorem is applied.
   For example, the theorem 
   @{thm [source] conjI} shown below can be used for any (typable) 
-  instantiation of @{text "?P"} and @{text "?Q"}. 
+  instantiation of \<open>?P\<close> and \<open>?Q\<close>. 
 
   @{ML_response_fake [display, gray]
   "pwriteln (pretty_thm @{context} @{thm conjI})"
@@ -213,16 +212,16 @@
 
   However, to improve the readability when printing theorems, we
   can switch off the question marks as follows:
-*}
+\<close>
 
-ML %grayML{*fun pretty_thm_no_vars ctxt thm =
+ML %grayML\<open>fun pretty_thm_no_vars ctxt thm =
 let
   val ctxt' = Config.put show_question_marks false ctxt
 in
   pretty_term ctxt' (Thm.prop_of thm)
-end*}
+end\<close>
 
-text {* 
+text \<open>
   With this function, theorem @{thm [source] conjI} is now printed as follows:
 
   @{ML_response_fake [display, gray]
@@ -231,31 +230,31 @@
   
   Again the functions @{ML commas} and @{ML block in Pretty} help 
   with printing more than one theorem. 
-*}
+\<close>
 
-ML %grayML{*fun pretty_thms ctxt thms =  
+ML %grayML\<open>fun pretty_thms ctxt thms =  
   Pretty.block (Pretty.commas (map (pretty_thm ctxt) thms))
 
 fun pretty_thms_no_vars ctxt thms =  
-  Pretty.block (Pretty.commas (map (pretty_thm_no_vars ctxt) thms))*}
+  Pretty.block (Pretty.commas (map (pretty_thm_no_vars ctxt) thms))\<close>
 
-text {*
+text \<open>
   Printing functions for @{ML_type typ} are
-*}
+\<close>
 
-ML %grayML{*fun pretty_typ ctxt ty = Syntax.pretty_typ ctxt ty
+ML %grayML\<open>fun pretty_typ ctxt ty = Syntax.pretty_typ ctxt ty
 fun pretty_typs ctxt tys = 
-  Pretty.block (Pretty.commas (map (pretty_typ ctxt) tys))*}
+  Pretty.block (Pretty.commas (map (pretty_typ ctxt) tys))\<close>
 
-text {*
+text \<open>
   respectively @{ML_type ctyp}
-*}
+\<close>
 
-ML %grayML{*fun pretty_ctyp ctxt cty = pretty_typ ctxt (Thm.typ_of cty)
+ML %grayML\<open>fun pretty_ctyp ctxt cty = pretty_typ ctxt (Thm.typ_of cty)
 fun pretty_ctyps ctxt ctys = 
-  Pretty.block (Pretty.commas (map (pretty_ctyp ctxt) ctys))*}
+  Pretty.block (Pretty.commas (map (pretty_ctyp ctxt) ctys))\<close>
 
-text {*
+text \<open>
   \begin{readmore}
   The simple conversion functions from Isabelle's main datatypes to 
   @{ML_type string}s are implemented in @{ML_file "Pure/Syntax/syntax.ML"}. 
@@ -298,12 +297,12 @@
   Most of the basic string functions of Isabelle are defined in 
   @{ML_file "Pure/library.ML"}.
   \end{readmore}
-*}
+\<close>
 
 
-section {* Combinators\label{sec:combinators} *}
+section \<open>Combinators\label{sec:combinators}\<close>
 
-text {*
+text \<open>
   For beginners perhaps the most puzzling parts in the existing code of
   Isabelle are the combinators. At first they seem to greatly obstruct the
   comprehension of code, but after getting familiar with them and handled with
@@ -311,37 +310,37 @@
 
   The simplest combinator is @{ML_ind I in Library}, which is just the 
   identity function defined as
-*}
+\<close>
 
-ML %grayML{*fun I x = x*}
+ML %grayML\<open>fun I x = x\<close>
 
-text {* 
+text \<open>
   Another simple combinator is @{ML_ind K in Library}, defined as 
-*}
+\<close>
 
-ML %grayML{*fun K x = fn _ => x*}
+ML %grayML\<open>fun K x = fn _ => x\<close>
 
-text {*
-  @{ML K} ``wraps'' a function around @{text "x"} that ignores its argument. As a 
-  result, @{ML K} defines a constant function always returning @{text x}.
+text \<open>
+  @{ML K} ``wraps'' a function around \<open>x\<close> that ignores its argument. As a 
+  result, @{ML K} defines a constant function always returning \<open>x\<close>.
 
   The next combinator is reverse application, @{ML_ind  "|>" in Basics}, defined as: 
-*}
+\<close>
 
-ML %grayML{*fun x |> f = f x*}
+ML %grayML\<open>fun x |> f = f x\<close>
 
-text {* While just syntactic sugar for the usual function application,
+text \<open>While just syntactic sugar for the usual function application,
   the purpose of this combinator is to implement functions in a  
-  ``waterfall fashion''. Consider for example the function *}
+  ``waterfall fashion''. Consider for example the function\<close>
 
-ML %linenosgray{*fun inc_by_five x =
+ML %linenosgray\<open>fun inc_by_five x =
   x |> (fn x => x + 1)
     |> (fn x => (x, x))
     |> fst
-    |> (fn x => x + 4)*}
+    |> (fn x => x + 4)\<close>
 
-text {*
-  which increments its argument @{text x} by 5. It does this by first
+text \<open>
+  which increments its argument \<open>x\<close> by 5. It does this by first
   incrementing the argument by 1 (Line 2); then storing the result in a pair
   (Line 3); taking the first component of the pair (Line 4) and finally
   incrementing the first component by 4 (Line 5). This kind of cascading
@@ -350,42 +349,42 @@
   manner. This kind of coding should be familiar, if you have been exposed to
   Haskell's {\it do}-notation. Writing the function @{ML inc_by_five} using
   the reverse application is much clearer than writing
-*}
+\<close>
 
-ML %grayML{*fun inc_by_five x = fst ((fn x => (x, x)) (x + 1)) + 4*}
+ML %grayML\<open>fun inc_by_five x = fst ((fn x => (x, x)) (x + 1)) + 4\<close>
 
-text {* or *}
+text \<open>or\<close>
 
-ML %grayML{*fun inc_by_five x = 
-  ((fn x => x + 4) o fst o (fn x => (x, x)) o (fn x => x + 1)) x*}
+ML %grayML\<open>fun inc_by_five x = 
+  ((fn x => x + 4) o fst o (fn x => (x, x)) o (fn x => x + 1)) x\<close>
 
-text {* and typographically more economical than *}
+text \<open>and typographically more economical than\<close>
 
-ML %grayML{*fun inc_by_five x =
+ML %grayML\<open>fun inc_by_five x =
 let val y1 = x + 1
     val y2 = (y1, y1)
     val y3 = fst y2
     val y4 = y3 + 4
-in y4 end*}
+in y4 end\<close>
 
-text {* 
+text \<open>
   Another reasons to avoid the let-bindings in the code above:
   it is easy to get the intermediate values wrong and
   the resulting code is difficult to maintain.
 
   In Isabelle a ``real world'' example for a function written in 
   the waterfall fashion might be the following code:
-*}
+\<close>
 
-ML %linenosgray{*fun apply_fresh_args f ctxt =
+ML %linenosgray\<open>fun apply_fresh_args f ctxt =
     f |> fastype_of
       |> binder_types 
       |> map (pair "z")
       |> Variable.variant_frees ctxt [f]
       |> map Free  
-      |> curry list_comb f *}
+      |> curry list_comb f\<close>
 
-text {*
+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 
   applied to it. For example, below three variables are applied to the term 
@@ -405,10 +404,10 @@
   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
   term; @{ML_ind binder_types in Term} in the next line produces the list of
-  argument types (in the case above the list @{text "[nat, int, unit]"}); Line
-  4 pairs up each type with the string @{text "z"}; the function @{ML_ind
-  variant_frees in Variable} generates for each @{text "z"} a unique name
-  avoiding the given @{text f}; the list of name-type pairs is turned into a
+  argument types (in the case above the list \<open>[nat, int, unit]\<close>); Line
+  4 pairs up each type with the string \<open>z\<close>; the function @{ML_ind
+  variant_frees in Variable} generates for each \<open>z\<close> a unique name
+  avoiding the given \<open>f\<close>; the list of name-type pairs is turned into a
   list of variable terms in Line 6, which in the last line is applied by the
   function @{ML_ind list_comb in Term} to the original term. In this last step we have
   to use the function @{ML_ind curry in Library}, because @{ML list_comb}
@@ -429,18 +428,18 @@
 end"
   "za z zb"}
   
-  where the @{text "za"} is correctly avoided.
+  where the \<open>za\<close> is correctly avoided.
 
   The combinator @{ML_ind "#>" in Basics} is the reverse function composition. 
   It can be used to define the following function
-*}
+\<close>
 
-ML %grayML{*val inc_by_six = 
+ML %grayML\<open>val inc_by_six = 
   (fn x => x + 1) #> 
   (fn x => x + 2) #> 
-  (fn x => x + 3)*}
+  (fn x => x + 3)\<close>
 
-text {* 
+text \<open>
   which is the function composed of first the increment-by-one function and
   then increment-by-two, followed by increment-by-three. Again, the reverse
   function composition allows you to read the code top-down. This combinator
@@ -451,18 +450,18 @@
   can be composed with @{ML "#>"}. 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>  
 
-local_setup %graylinenos {* 
+local_setup %graylinenos \<open>
 let  
   fun my_note name thm = Local_Theory.note ((name, []), [thm]) #> snd
 in
   my_note @{binding "foo_conjI"} @{thm conjI} #>
   my_note @{binding "bar_conjunct1"} @{thm conjunct1} #>
   my_note @{binding "bar_conjunct2"} @{thm conjunct2}
-end *}
+end\<close>
 
-text {*
+text \<open>
   The function @{ML_text "my_note"} in line 3 is just a wrapper for the function 
   @{ML_ind note in Local_Theory} in the structure @{ML_struct Local_Theory}; 
   it stores a theorem under a name. 
@@ -474,15 +473,15 @@
   in Basics} allows you to get hold of an intermediate result (to do some
   side-calculations or print out an intermediate result, for instance). The
   function
- *}
+\<close>
 
-ML %linenosgray{*fun inc_by_three x =
+ML %linenosgray\<open>fun inc_by_three x =
      x |> (fn x => x + 1)
        |> tap (fn x => pwriteln (Pretty.str (@{make_string} x)))
-       |> (fn x => x + 2)*}
+       |> (fn x => x + 2)\<close>
 
-text {* 
-  increments the argument first by @{text "1"} and then by @{text "2"}. In the
+text \<open>
+  increments the argument first by \<open>1\<close> and then by \<open>2\<close>. In the
   middle (Line 3), however, it uses @{ML tap} for printing the ``plus-one''
   intermediate result. The function @{ML tap} can only be used for
   side-calculations, because any value that is computed cannot be merged back
@@ -491,102 +490,102 @@
   The combinator @{ML_ind "`" in Basics} (a backtick) is similar to @{ML tap},
   but applies a function to the value and returns the result together with the
   value (as a pair). It is defined as
-*}
+\<close>
 
-ML %grayML{*fun `f = fn x => (f x, x)*}
+ML %grayML\<open>fun `f = fn x => (f x, x)\<close>
 
-text {*
+text \<open>
   An example for this combinator is the function
-*}
+\<close>
 
-ML %grayML{*fun inc_as_pair x =
+ML %grayML\<open>fun inc_as_pair x =
      x |> `(fn x => x + 1)
-       |> (fn (x, y) => (x, y + 1))*}
+       |> (fn (x, y) => (x, y + 1))\<close>
 
-text {*
-  which takes @{text x} as argument, and then increments @{text x}, but also keeps
-  @{text x}. The intermediate result is therefore the pair @{ML "(x + 1, x)"
+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)"
   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}.
 
   The combinators @{ML_ind "|>>" in Basics} and @{ML_ind "||>" in Basics} are
   defined for functions manipulating pairs. The first applies the function to
   the first component of the pair, defined as
-*}
+\<close>
 
-ML %grayML{*fun (x, y) |>> f = (f x, y)*}
+ML %grayML\<open>fun (x, y) |>> f = (f x, y)\<close>
 
-text {*
+text \<open>
   and the second combinator to the second component, defined as
-*}
+\<close>
 
-ML %grayML{*fun (x, y) ||> f = (x, f y)*}
+ML %grayML\<open>fun (x, y) ||> f = (x, f y)\<close>
 
-text {*
-  These two functions can, for example, be used to avoid explicit @{text "lets"} for
+text \<open>
+  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
   implemented as
-*}
+\<close>
 
-ML %grayML{*fun separate i [] = ([], [])
+ML %grayML\<open>fun separate i [] = ([], [])
   | separate i (x::xs) =
       let 
         val (los, grs) = separate i xs
       in
         if i <= x then (los, x::grs) else (x::los, grs)
-      end*}
+      end\<close>
 
-text {*
+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
   can be implemented more concisely as
-*}
+\<close>
 
-ML %grayML{*fun separate _ [] = ([], [])
+ML %grayML\<open>fun separate _ [] = ([], [])
   | separate i (x::xs) =
       if i <= x 
       then separate i xs ||> cons x
-      else separate i xs |>> cons x*}
+      else separate i xs |>> cons x\<close>
 
-text {*
-  avoiding the explicit @{text "let"}. While in this example the gain in
+text \<open>
+  avoiding the explicit \<open>let\<close>. While in this example the gain in
   conciseness is only small, in more complicated situations the benefit of
-  avoiding @{text "lets"} can be substantial.
+  avoiding \<open>lets\<close> can be substantial.
 
   With the combinator @{ML_ind "|->" in Basics} you can re-combine the 
   elements from a pair. This combinator is defined as
-*}
+\<close>
 
-ML %grayML{*fun (x, y) |-> f = f x y*}
+ML %grayML\<open>fun (x, y) |-> f = f x y\<close>
 
-text {* 
+text \<open>
   and can be used to write the following roundabout version 
-  of the @{text double} function: 
-*}
+  of the \<open>double\<close> function: 
+\<close>
 
-ML %grayML{*fun double x =
+ML %grayML\<open>fun double x =
       x |>  (fn x => (x, x))
-        |-> (fn x => fn y => x + y)*}
+        |-> (fn x => fn y => x + y)\<close>
 
-text {* 
+text \<open>
   The combinator @{ML_ind ||>> in Basics} plays a central role whenever your
   task is to update a theory and the update also produces a side-result (for
   example a theorem). Functions for such tasks return a pair whose second
   component is the theory and the fist component is the side-result. Using
   @{ML ||>>}, you can do conveniently the update and also
   accumulate the side-results. Consider the following simple function.
-*}
+\<close>
 
-ML %linenosgray{*fun acc_incs x =
+ML %linenosgray\<open>fun acc_incs x =
     x |> (fn x => ("", x)) 
       ||>> (fn x => (x, x + 1))
       ||>> (fn x => (x, x + 1))
-      ||>> (fn x => (x, x + 1))*}
+      ||>> (fn x => (x, x + 1))\<close>
 
-text {*
+text \<open>
   The purpose of Line 2 is to just pair up the argument with a dummy value (since
   @{ML ||>>} operates on pairs). Each of the next three lines just increment 
   the value by one, but also nest the intermediate results to the left. For example 
@@ -626,15 +625,15 @@
   obtained by previous calls.
   
   A more realistic example for this combinator is the following code
-*}
+\<close>
 
-ML %grayML{*val ((([one_def], [two_def]), [three_def]), ctxt') = 
+ML %grayML\<open>val ((([one_def], [two_def]), [three_def]), ctxt') = 
   @{context}
   |> Local_Defs.define [((@{binding "One"}, NoSyn), (Binding.empty_atts, @{term "1::nat"}))]
   ||>> Local_Defs.define [((@{binding "Two"}, NoSyn), (Binding.empty_atts,@{term "2::nat"}))]
-  ||>> Local_Defs.define [((@{binding "Three"}, NoSyn), (Binding.empty_atts,@{term "3::nat"}))]*}
+  ||>> Local_Defs.define [((@{binding "Three"}, NoSyn), (Binding.empty_atts,@{term "3::nat"}))]\<close>
 
-text {*
+text \<open>
   where we make three definitions, namely @{term "One \<equiv> 1::nat"}, @{term "Two \<equiv> 2::nat"}
   and @{term "Three \<equiv> 3::nat"}. The point of this code is that we augment the initial
   context with the definitions. The result we are interested in is the
@@ -658,15 +657,15 @@
   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
-  function @{text double} can also be written as:
-*}
+  function \<open>double\<close> can also be written as:
+\<close>
 
-ML %grayML{*val double =
+ML %grayML\<open>val double =
    (fn x => (x, x)) #-> 
-   (fn x => fn y => x + y)*}
+   (fn x => fn y => x + y)\<close>
 
 
-text {* 
+text \<open>
   When using combinators for writing functions in waterfall fashion, it is
   sometimes necessary to do some ``plumbing'' in order to fit functions
   together. We have already seen such plumbing in the function @{ML
@@ -687,11 +686,11 @@
   |> pwriteln
 end"
   "m + n, m * n, m - n"}
-*}
+\<close>
 
-text {*
+text \<open>
   In this example we obtain three terms (using the function 
-  @{ML_ind parse_term in Syntax}) whose variables @{text m} and @{text n} 
+  @{ML_ind parse_term in Syntax}) whose variables \<open>m\<close> and \<open>n\<close> 
   are of type @{typ "nat"}. If you have only a single term, then @{ML
   check_terms in Syntax} needs plumbing. This can be done with the function
   @{ML_ind singleton in Library}.\footnote{There is already a function @{ML check_term in
@@ -722,12 +721,12 @@
   \begin{exercise}
   Find out what the combinator @{ML "K I"} does.
   \end{exercise}
-*}
+\<close>
 
 
-section {* ML-Antiquotations\label{sec:antiquote} *}
+section \<open>ML-Antiquotations\label{sec:antiquote}\<close>
 
-text {*
+text \<open>
   Recall from Section \ref{sec:include} that code in Isabelle is always
   embedded in a theory.  The main advantage of this is that the code can
   contain references to entities defined on the logical level of Isabelle. By
@@ -744,33 +743,32 @@
   user level and therefore we are not interested in them in this Tutorial,
   except in Appendix \ref{rec:docantiquotations} where we show how to
   implement your own document antiquotations.}  Syntactically antiquotations
-  are indicated by the @{ML_text @}-sign followed by text wrapped in @{text
-  "{\<dots>}"}.  For example, one can print out the name of the current theory with
+  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_response [display,gray] "Context.theory_name @{theory}" "\"First_Steps\""}
  
-  where @{text "@{theory}"} is an antiquotation that is substituted with the
+  where \<open>@{theory}\<close> is an antiquotation that is substituted with the
   current theory (remember that we assumed we are inside the theory 
-  @{text First_Steps}). The name of this theory can be extracted using
+  \<open>First_Steps\<close>). The name of this theory can be extracted using
   the function @{ML_ind theory_name in Context}. 
 
   Note, however, that antiquotations are statically linked, that is their value is
   determined at ``compile-time'', not at ``run-time''. For example the function
-*}
+\<close>
 
-ML %grayML{*fun not_current_thyname () = Context.theory_name @{theory} *}
+ML %grayML\<open>fun not_current_thyname () = Context.theory_name @{theory}\<close>
 
-text {*
+text \<open>
   does \emph{not} return the name of the current theory, if it is run in a 
   different theory. Instead, the code above defines the constant function 
   that always returns the string @{text [quotes] "First_Steps"}, no matter where the
-  function is called. Operationally speaking,  the antiquotation @{text "@{theory}"} is 
+  function is called. Operationally speaking,  the antiquotation \<open>@{theory}\<close> is 
   \emph{not} replaced with code that will look up the current theory in 
   some data structure and return it. Instead, it is literally
   replaced with the value representing the theory.
 
-  Another important antiquotation is @{text "@{context}"}. (What the
+  Another important antiquotation is \<open>@{context}\<close>. (What the
   difference between a theory and a context is will be described in Chapter
   \ref{chp:advanced}.) A context is for example needed to use the
   function @{ML print_abbrevs in Proof_Context} that list of all currently
@@ -786,11 +784,11 @@
   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: 
-  @{text "@{thm \<dots>}"} for a single theorem
+  \<open>@{thm \<dots>}\<close> for a single theorem
 
   @{ML_response_fake [display,gray] "@{thm allI}" "(\<And>x. ?P x) \<Longrightarrow> \<forall>x. ?P x"}
 
-  and @{text "@{thms \<dots>}"} for more than one
+  and \<open>@{thms \<dots>}\<close> for more than one
 
 @{ML_response_fake [display,gray] 
   "@{thms conj_ac}" 
@@ -811,14 +809,14 @@
   under this name (this becomes especially important when you deal with
   theorem lists; see Section \ref{sec:storing}).
 
-  It is also possible to prove lemmas with the antiquotation @{text "@{lemma \<dots> by \<dots>}"}
-  whose first argument is a statement (possibly many of them separated by @{text "and"})
+  It is also possible to prove lemmas with the antiquotation \<open>@{lemma \<dots> by \<dots>}\<close>
+  whose first argument is a statement (possibly many of them separated by \<open>and\<close>)
   and the second is a proof. For example
-*}
+\<close>
 
-ML %grayML{*val foo_thms = @{lemma "True" and "False \<Longrightarrow> P" by simp_all} *}
+ML %grayML\<open>val foo_thms = @{lemma "True" and "False \<Longrightarrow> P" by simp_all}\<close>
 
-text {*
+text \<open>
   The result can be printed out as follows.
 
   @{ML_response_fake [gray,display]
@@ -829,17 +827,17 @@
   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 
   simpset.
-*}
+\<close>
 
-ML %grayML{*fun get_thm_names_from_ss ctxt =
+ML %grayML\<open>fun get_thm_names_from_ss ctxt =
 let
   val simpset = Raw_Simplifier.simpset_of ctxt
   val {simps,...} = Raw_Simplifier.dest_ss simpset
 in
   map #1 simps
-end*}
+end\<close>
 
-text {*
+text \<open>
   The function @{ML_ind dest_ss in Raw_Simplifier} returns a record containing all
   information stored in the simpset, but here we are only interested in the names of the
   simp-rules. Now you can feed in the current simpset into this function. 
@@ -856,15 +854,15 @@
   It is also possible to define your own antiquotations. But you should
   exercise care when introducing new ones, as they can also make your code
   difficult to read. In the next chapter we describe how to construct
-  terms with the (built-in) antiquotation @{text "@{term \<dots>}"}.  A restriction
+  terms with the (built-in) antiquotation \<open>@{term \<dots>}\<close>.  A restriction
   of this antiquotation is that it does not allow you to use schematic
   variables in terms. If you want to have an antiquotation that does not have
   this restriction, you can implement your own using the function @{ML_ind
   inline in ML_Antiquotation} from the structure @{ML_struct ML_Antiquotation}. The code
-  for the antiquotation @{text "term_pat"} is as follows.
-*}
+  for the antiquotation \<open>term_pat\<close> is as follows.
+\<close>
 
-ML %linenosgray{*val term_pat_setup = 
+ML %linenosgray\<open>val term_pat_setup = 
 let
   val parser = Args.context -- Scan.lift Args.embedded_inner_syntax
 
@@ -874,15 +872,15 @@
          |> ML_Syntax.atomic
 in
   ML_Antiquotation.inline @{binding "term_pat"} (parser >> term_pat)
-end*}
+end\<close>
 
-text {*
+text \<open>
   To use it you also have to install it using \isacommand{setup} like so
-*}
+\<close>
 
-setup %gray {* term_pat_setup *}
+setup %gray \<open>term_pat_setup\<close>
 
-text {*
+text \<open>
   The parser in Line 2 provides us with a context and a string; this string is
   transformed into a term using the function @{ML_ind read_term_pattern in
   Proof_Context} (Line 5); the next two lines transform the term into a string
@@ -893,11 +891,11 @@
   "@{term_pat \"Suc (?x::nat)\"}"
   "Const (\"Suc\", \"nat \<Rightarrow> nat\") $ Var ((\"x\", 0), \"nat\")"}
 
-  which shows the internal representation of the term @{text "Suc ?x"}. Similarly
+  which shows the internal representation of the term \<open>Suc ?x\<close>. Similarly
   we can write an antiquotation for type patterns. Its code is
-*}
+\<close>
 
-ML %grayML{*val type_pat_setup = 
+ML %grayML\<open>val type_pat_setup = 
 let
   val parser = Args.context -- Scan.lift Args.embedded_inner_syntax
 
@@ -911,15 +909,15 @@
       end
 in
   ML_Antiquotation.inline @{binding "typ_pat"} (parser >> typ_pat)
-end*}
+end\<close>
 
-text {*
+text \<open>
   which can be installed with
-*}
+\<close>
 
-setup %gray {* type_pat_setup *}
+setup %gray \<open>type_pat_setup\<close>
 
-text {* 
+text \<open>
 However, a word of warning is in order: new antiquotations should be introduced only after
 careful deliberations. They can potentially make your code harder, rather than easier, to read.
 
@@ -928,11 +926,11 @@
   contain the infrastructure and definitions for most antiquotations. Most of the basic operations 
   on ML-syntax are implemented in @{ML_file "Pure/ML/ml_syntax.ML"}.
   \end{readmore}
-*}
+\<close>
 
-section {* Storing Data in Isabelle\label{sec:storing} *}
+section \<open>Storing Data in Isabelle\label{sec:storing}\<close>
 
-text {*
+text \<open>
   Isabelle provides mechanisms for storing (and retrieving) arbitrary
   data. Before we delve into the details, let us digress a bit. Conventional
   wisdom has it that the type-system of ML ensures that  an
@@ -956,9 +954,9 @@
   We will show the usage of the universal type by storing an integer and
   a boolean into a single list. Let us first define injection and projection 
   functions for booleans and integers into and from the type @{ML_type Universal.universal}.
-*}
+\<close>
 
-ML %grayML{*local
+ML %grayML\<open>local
   val fn_int  = Universal.tag () : int  Universal.tag
   val fn_bool = Universal.tag () : bool Universal.tag
 in
@@ -966,23 +964,23 @@
   val inject_bool  = Universal.tagInject fn_bool;
   val project_int  = Universal.tagProject fn_int;
   val project_bool = Universal.tagProject fn_bool
-end*}
+end\<close>
 
-text {*
+text \<open>
   Using the injection functions, we can inject the integer @{ML_text "13"} 
   and the boolean value @{ML_text "true"} into @{ML_type Universal.universal}, and
   then store them in a @{ML_type "Universal.universal list"} as follows:
-*}
+\<close>
 
-ML %grayML{*val foo_list = 
+ML %grayML\<open>val foo_list = 
 let
   val thirteen = inject_int 13
   val truth_val = inject_bool true
 in
   [thirteen, truth_val]
-end*}
+end\<close>
 
-text {*
+text \<open>
   The data can be retrieved with the projection functions defined above.
   
   @{ML_response_fake [display, gray]
@@ -1023,15 +1021,15 @@
   and therefore it makes sense to store this data inside a theory.  
   Consequently we use the functor @{ML_funct Theory_Data}.
   The code for the table is:
-*}
+\<close>
 
-ML %linenosgray{*structure Data = Theory_Data
+ML %linenosgray\<open>structure Data = Theory_Data
   (type T = thm Symtab.table
    val empty = Symtab.empty
    val extend = I
-   val merge = Symtab.merge (K true))*}
+   val merge = Symtab.merge (K true))\<close>
 
-text {*
+text \<open>
   In order to store data in a theory, we have to specify the type of the data
   (Line 2). In this case we specify the type @{ML_type "thm Symtab.table"},
   which stands for a table in which @{ML_type string}s can be looked up
@@ -1046,23 +1044,23 @@
   it (@{ML Data.map}). There is also the function @{ML Data.put}, but it is 
   not relevant here. Below we define two
   auxiliary functions, which help us with accessing the table.
-*}
+\<close>
 
-ML %grayML{*val lookup = Symtab.lookup o Data.get
-fun update k v = Data.map (Symtab.update (k, v))*}
+ML %grayML\<open>val lookup = Symtab.lookup o Data.get
+fun update k v = Data.map (Symtab.update (k, v))\<close>
 
-text {*
+text \<open>
   Since we want to store introduction rules associated with their 
   logical connective, we can fill the table as follows.
-*}
+\<close>
 
-setup %gray {*
+setup %gray \<open>
   update "conj" @{thm conjI} #>
   update "imp"  @{thm impI}  #>
   update "all"  @{thm allI}
-*}
+\<close>
 
-text {*
+text \<open>
   The use of the command \isacommand{setup} makes sure the table in the 
   \emph{current} theory is updated (this is explained further in 
   Section~\ref{sec:theories}). The lookup can now be performed as follows.
@@ -1074,11 +1072,11 @@
   An important point to note is that these tables (and data in general)
   need to be treated in a purely functional fashion. Although
   we can update the table as follows
-*}
+\<close>
 
-setup %gray {* update "conj" @{thm TrueI} *}
+setup %gray \<open>update "conj" @{thm TrueI}\<close>
 
-text {*
+text \<open>
   and accordingly, @{ML lookup} now produces the introduction rule for @{term "True"}
   
 @{ML_response_fake [display, gray]
@@ -1091,15 +1089,15 @@
   defeat its undo-mechanism. To see the latter, consider the 
   following data container where we maintain a reference to a list of 
   integers.
-*}
+\<close>
 
-ML %grayML{*structure WrongRefData = Theory_Data
+ML %grayML\<open>structure WrongRefData = Theory_Data
   (type T = (int list) Unsynchronized.ref
    val empty = Unsynchronized.ref []
    val extend = I
-   val merge = fst)*}
+   val merge = fst)\<close>
 
-text {*
+text \<open>
   We initialise the reference with the empty list. Consequently a first 
   lookup produces @{ML "ref []" in Unsynchronized}.
 
@@ -1108,20 +1106,20 @@
   "ref []"}
 
   For updating the reference we use the following function
-*}
+\<close>
 
-ML %grayML{*fun ref_update n = WrongRefData.map 
-      (fn r => let val _ = r := n::(!r) in r end)*}
+ML %grayML\<open>fun ref_update n = WrongRefData.map 
+      (fn r => let val _ = r := n::(!r) in r end)\<close>
 
-text {*
+text \<open>
   which takes an integer and adds it to the content of the reference.
   As before, we update the reference with the command 
   \isacommand{setup}. 
-*}
+\<close>
 
-setup %gray {* ref_update 1 *}
+setup %gray \<open>ref_update 1\<close>
 
-text {*
+text \<open>
   A lookup in the current theory gives then the expected list 
   @{ML "ref [1]" in Unsynchronized}.
 
@@ -1159,30 +1157,30 @@
   Storing data in a proof context is done in a similar fashion. As mentioned
   before, the corresponding functor is @{ML_funct_ind Proof_Data}. With the
   following code we can store a list of terms in a proof context.
-*}
+\<close>
 
-ML %grayML{*structure Data = Proof_Data
+ML %grayML\<open>structure Data = Proof_Data
   (type T = term list
-   fun init _ = [])*}
+   fun init _ = [])\<close>
 
-text {*
+text \<open>
   The init-function we have to specify must produce a list for when a context 
   is initialised (possibly taking the theory into account from which the 
   context is derived). We choose here to just return the empty list. Next 
   we define two auxiliary functions for updating the list with a given
   term and printing the list. 
-*}
+\<close>
 
-ML %grayML{*fun update trm = Data.map (fn trms => trm::trms)
+ML %grayML\<open>fun update trm = Data.map (fn trms => trm::trms)
 
 fun print ctxt =
   case (Data.get ctxt) of
     [] => pwriteln (Pretty.str "Empty!")
-  | trms => pwriteln (pretty_terms ctxt trms)*}
+  | trms => pwriteln (pretty_terms ctxt trms)\<close>
 
-text {*
+text \<open>
   Next we start with the context generated by the antiquotation 
-  @{text "@{context}"} and update it in various ways. 
+  \<open>@{context}\<close> and update it in various ways. 
 
   @{ML_response_fake [display,gray]
 "let
@@ -1216,63 +1214,63 @@
 
   For convenience there is an abstract layer, namely the type @{ML_type Context.generic}, 
   for treating theories and proof contexts more uniformly. This type is defined as follows
-*}
+\<close>
 
-ML_val %grayML{*datatype generic = 
+ML_val %grayML\<open>datatype generic = 
   Theory of theory 
-| Proof of proof*}
+| Proof of proof\<close>
 
-text {*
+text \<open>
   \footnote{\bf FIXME: say more about generic contexts.}
 
   There are two special instances of the data storage mechanism described 
   above. The first instance implements named theorem lists using the functor
   @{ML_funct_ind Named_Thms}. This is because storing theorems in a list 
   is such a common task.  To obtain a named theorem list, you just declare
-*}
+\<close>
 
-ML %grayML{*structure FooRules = Named_Thms
+ML %grayML\<open>structure FooRules = Named_Thms
   (val name = @{binding "foo"} 
-   val description = "Theorems for foo") *}
+   val description = "Theorems for foo")\<close>
 
-text {*
+text \<open>
   and set up the @{ML_struct FooRules} with the command
-*}
+\<close>
 
-setup %gray {* FooRules.setup *}
+setup %gray \<open>FooRules.setup\<close>
 
-text {*
+text \<open>
   This code declares a data container where the theorems are stored,
-  an attribute @{text foo} (with the @{text add} and @{text del} options
+  an attribute \<open>foo\<close> (with the \<open>add\<close> and \<open>del\<close> options
   for adding and deleting theorems) and an internal ML-interface for retrieving and 
   modifying the theorems.
   Furthermore, the theorems are made available on the user-level under the name 
-  @{text foo}. For example you can declare three lemmas to be a member of the 
-  theorem list @{text foo} by:
-*}
+  \<open>foo\<close>. For example you can declare three lemmas to be a member of the 
+  theorem list \<open>foo\<close> by:
+\<close>
 
 lemma rule1[foo]: "A" sorry
 lemma rule2[foo]: "B" sorry
 lemma rule3[foo]: "C" sorry
 
-text {* and undeclare the first one by: *}
+text \<open>and undeclare the first one by:\<close>
 
 declare rule1[foo del]
 
-text {* You can query the remaining ones with:
+text \<open>You can query the remaining ones with:
 
   \begin{isabelle}
-  \isacommand{thm}~@{text "foo"}\\
-  @{text "> ?C"}\\
-  @{text "> ?B"}
+  \isacommand{thm}~\<open>foo\<close>\\
+  \<open>> ?C\<close>\\
+  \<open>> ?B\<close>
   \end{isabelle}
 
   On the ML-level, we can add theorems to the list with @{ML FooRules.add_thm}:
-*} 
+\<close> 
 
-setup %gray {* Context.theory_map (FooRules.add_thm @{thm TrueI}) *}
+setup %gray \<open>Context.theory_map (FooRules.add_thm @{thm TrueI})\<close>
 
-text {*
+text \<open>
   The rules in the list can be retrieved using the function 
   @{ML FooRules.get}:
 
@@ -1293,24 +1291,23 @@
   The second special instance of the data storage mechanism are configuration
   values. They are used to enable users to configure tools without having to
   resort to the ML-level (and also to avoid references). Assume you want the
-  user to control three values, say @{text bval} containing a boolean, @{text
-  ival} containing an integer and @{text sval} containing a string. These
+  user to control three values, say \<open>bval\<close> containing a boolean, \<open>ival\<close> containing an integer and \<open>sval\<close> containing a string. These
   values can be declared by
-*}
+\<close>
 
-ML %grayML{*val bval = Attrib.setup_config_bool @{binding "bval"} (K false)
+ML %grayML\<open>val bval = Attrib.setup_config_bool @{binding "bval"} (K false)
 val ival = Attrib.setup_config_int @{binding "ival"} (K 0)
-val sval = Attrib.setup_config_string @{binding "sval"} (K "some string") *}
+val sval = Attrib.setup_config_string @{binding "sval"} (K "some string")\<close>
 
-text {* 
+text \<open>
   where each value needs to be given a default. 
   The user can now manipulate the values from the user-level of Isabelle 
   with the command
-*}
+\<close>
 
 declare [[bval = true, ival = 3]]
 
-text {*
+text \<open>
   On the ML-level these values can be retrieved using the 
   function @{ML_ind get in Config} from a proof context
 
@@ -1343,7 +1340,7 @@
   A concrete example for a configuration value is 
   @{ML_ind simp_trace in Raw_Simplifier}, which switches on trace information
   in the simplifier. This can be used for example in the following proof
-*}
+\<close>
 
 
 lemma
@@ -1354,7 +1351,7 @@
   show "True" by simp
 qed
 
-text {*
+text \<open>
   in order to inspect how the simplifier solves the first subgoal.
 
   \begin{readmore}
@@ -1362,11 +1359,11 @@
   the files @{ML_file "Pure/Isar/attrib.ML"} and 
   @{ML_file "Pure/config.ML"}.
   \end{readmore}
-*}
+\<close>
 
-section {* Summary *}
+section \<open>Summary\<close>
 
-text {*
+text \<open>
   This chapter describes the combinators that are used in Isabelle, as well
   as a simple printing infrastructure for @{ML_type term}, @{ML_type cterm}
   and @{ML_type thm}. The section on ML-antiquotations shows how to refer 
@@ -1381,5 +1378,5 @@
   \end{itemize}
   \end{conventions}
 
-*}
+\<close>
 end




