isabelle-cookbook: comparison ProgTutorial/First

equal deleted inserted replaced

-:6e2479089226
+:cecd7a941885
 theory First_Steps
 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]
 Brian Kernighan, in {\em Unix for Beginners}, 1979
 \end{flushright}
 \end{tabular}
 \end{quote}
 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
+\<open>\<verbclose>\<close>\isanewline
-@{text "> 7"}\smallskip
+\<open>> 7\<close>\smallskip
 \end{graybox}
 \end{isabelle}
 If you work with ProofGeneral then like normal Isabelle scripts
 \isacommand{ML}-commands can be evaluated by using the advance and
 undo buttons of your Isabelle environment.  If you work with the
 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
+As mentioned in the Introduction, we will drop the \isacommand{ML}~\<open>\<verbopen> \<dots> \<verbclose>\<close> scaffolding whenever we show code. The lines
-"\<verbopen> \<dots> \<verbclose>"} 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
 ML-code. The first evaluates the given code, but any effect on the theory,
 in which the code is embedded, is suppressed. The second needs to be used if
 ML-code is defined inside a proof. For example
 \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}
 However, both commands will only play minor roles in this tutorial (we most of
 \begin{tabular}{@ {}l}
 \isacommand{theory} First\_Steps\\
 \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
 @{ML_response_fake [display,gray] "writeln \"any string\"" "\"any string\""}
 will print out @{text [quotes] "any string"}.
 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};
 for example:
 @{ML_response_fake [display,gray]
 "if 0 = 1 then true else (error \"foo\")"
 "*** 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}
 and @{ML_type thm}. Isabelle provides elaborate pretty-printing functions,
 which we will explain in more detail in Section \ref{sec:pretty}. For now
 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
+ML %grayML\<open>val pretty_term = Syntax.pretty_term
-val pwriteln = Pretty.writeln*}
+val pwriteln = Pretty.writeln\<close>
-text {*
+text \<open>
 They can be used as follows
 @{ML_response_fake [display,gray]
 "pwriteln (pretty_term @{context} @{term \"1::nat\"})"
 "\"1\""}
 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 =
+ML %grayML\<open>fun pretty_terms ctxt trms =
-Pretty.block (Pretty.commas (map (pretty_term 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
 \begin{itemize}
 \item @{ML_ind show_brackets in Syntax}
 \item @{ML_ind show_sorts in Syntax}
 \item @{ML_ind eta_contract in Syntax}
 \end{itemize}
 A @{ML_type cterm} can be printed with the following function.
-*}
+\<close>
-ML %grayML %grayML{*fun pretty_cterm ctxt ctrm =
+ML %grayML %grayML\<open>fun pretty_cterm ctxt ctrm =
-pretty_term ctxt (Thm.term_of 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 =
+ML %grayML\<open>fun pretty_cterms ctxt ctrms =
-Pretty.block (Pretty.commas (map (pretty_cterm 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 =
+ML %grayML\<open>fun pretty_thm ctxt thm =
-pretty_term ctxt (Thm.prop_of thm)*}
+pretty_term ctxt (Thm.prop_of thm)\<close>
-text {*
+text \<open>
-Theorems include schematic variables, such as @{text "?P"},
+Theorems include schematic variables, such as \<open>?P\<close>,
-@{text "?Q"} and so on. They are instantiated by Isabelle when a theorem is applied.
+\<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})"
 "\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q"}
 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]
 "pwriteln (pretty_thm_no_vars @{context} @{thm conjI})"
 "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> P \<and> Q"}
 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"}.
 The configuration values that change the printing information are declared in
 @{ML_file "Pure/Syntax/printer.ML"}.
 \begin{readmore}
 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
 care, they actually ease the understanding and also the programming.
 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 {*
+text \<open>
-@{ML K} ``wraps'' a function around @{text "x"} that ignores its argument. As a
+@{ML K} ``wraps'' a function around \<open>x\<close> that ignores its argument. As a
-result, @{ML K} defines a constant function always returning @{text x}.
+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 {*
+text \<open>
-which increments its argument @{text x} by 5. It does this by first
+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
 manipulations of values is quite common when dealing with theories. The
 reverse application allows you to read what happens in a top-down
 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 =
+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*}
+((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
 @{term [show_types] "P::nat \<Rightarrow> int \<Rightarrow> unit \<Rightarrow> bool"}:
 "P z za zb"}
 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
+argument types (in the case above the list \<open>[nat, int, unit]\<close>); Line
-4 pairs up each type with the string @{text "z"}; the function @{ML_ind
+4 pairs up each type with the string \<open>z\<close>; the function @{ML_ind
-variant_frees in Variable} generates for each @{text "z"} a unique name
+variant_frees in Variable} generates for each \<open>z\<close> a unique name
-avoiding the given @{text f}; the list of name-type pairs is turned into a
+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}
 expects the function and the variables list as a pair.
 |> pretty_term ctxt
 |> pwriteln
 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
 is often used for setup functions inside the
 \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,
 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.
 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.
 The remaining combinators we describe in this section add convenience for
 the ``waterfall method'' of writing functions. The combinator @{ML_ind tap
 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 {*
+text \<open>
-increments the argument first by @{text "1"} and then by @{text "2"}. In the
+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
 into the ``main waterfall''. To do this, you can use the next combinator.
 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 {*
+text \<open>
-which takes @{text x} as argument, and then increments @{text x}, but also keeps
+which takes \<open>x\<close> as argument, and then increments \<open>x\<close>, but also keeps
-@{text x}. The intermediate result is therefore the pair @{ML "(x + 1, x)"
+\<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 {*
+text \<open>
-These two functions can, for example, be used to avoid explicit @{text "lets"} for
+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 {*
+text \<open>
-avoiding the explicit @{text "let"}. While in this example the gain in
+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
 @{ML_response [display,gray]
 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)
 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
 augmented context, that is @{ML_text "ctxt'"}, but also the side-results containing
 information about the definitions---the function @{ML_ind define in Local_Defs} returns
 the related reverse function composition is @{ML "#>"}. In fact all the
 combinators @{ML "|->"}, @{ML "|>>"} , @{ML "||>"} and @{ML "||>>"}
 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
 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
 |> Syntax.check_terms ctxt
 |> pretty_terms ctxt
 |> 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
 Syntax} in the file @{ML_file "Pure/Syntax/syntax.ML"} that is implemented
 in terms of @{ML singleton} and @{ML check_terms in Syntax}.} For example
 \end{readmore}
 \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
 this we mean references to definitions, theorems, terms and so on. These
 reference are realised in Isabelle with ML-antiquotations, often just called
 only in the text parts of Isabelle and their purpose is to print logical
 entities inside \LaTeX-documents. Document antiquotations are part of the
 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
+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
-"{\<dots>}"}.  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
 defined abbreviations. For example
 \<dots>"}
 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}"
 "(?P \<and> ?Q) = (?Q \<and> ?P)
 (?P \<and> ?Q \<and> ?R) = (?Q \<and> ?P \<and> ?R)
 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
 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>}"}
+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 @{text "and"})
+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]
 "foo_thms |> pretty_thms_no_vars @{context}
 |> pwriteln"
 "True, False \<Longrightarrow> P"}
 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.
 The current simpset can be referred to using @{ML_ind simpset_of in Raw_Simplifier}.
 code.
 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
 fun term_pat (ctxt, str) =
 str |> Proof_Context.read_term_pattern ctxt
 |> ML_Syntax.print_term
 |> 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
 so that the ML-system can understand it. (All these functions will be explained
 in more detail in later sections.) An example for this antiquotation is:
 @{ML_response_fake [display,gray]
 "@{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
 fun typ_pat (ctxt, str) =
 let
 |> ML_Syntax.print_typ
 |> ML_Syntax.atomic
 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.
 \begin{readmore} @{url "Norbert/ML/ml_antiquotation.ML"}
 The files @{ML_file "Pure/ML/ml_antiquotation.ML"} and @{ML_file "Pure/ML/ml_antiquotations.ML"}
 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
 @{ML_type "'a list"}, say, can only hold elements of the same type, namely
 @{ML_type "'a"} (or whatever is substitued for it). Despite this common
 \end{readmore}
 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
 val inject_int   = Universal.tagInject fn_int;
 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]
 "project_int (nth foo_list 0);
 project_bool (nth foo_list 1)"
 intention in this example is to be able to look up introduction rules for logical
 connectives. Such a table might be useful in an automatic proof procedure
 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
 producing an associated @{ML_type thm}. We also have to specify four
 functions to use this functor: namely how to initialise the data storage
 assumptions of these operations.} The result structure @{ML_text Data}
 contains functions for accessing the table (@{ML Data.get}) and for updating
 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
+ML %grayML\<open>val lookup = Symtab.lookup o Data.get
-fun update k v = Data.map (Symtab.update (k, v))*}
+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.
 @{ML_response_fake [display, gray]
 "SOME \"\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q\""}
 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]
 "lookup @{theory} \"conj\""
 "SOME \"True\""}
 coding conventions for programming in Isabelle. References
 interfere with the multithreaded execution model of Isabelle and also
 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}.
 @{ML_response_fake [display,gray]
 "WrongRefData.get @{theory}"
 "ref []"}
 For updating the reference we use the following function
-*}
+\<close>
-ML %grayML{*fun ref_update n = WrongRefData.map
+ML %grayML\<open>fun ref_update n = WrongRefData.map
-(fn r => let val _ = r := n::(!r) in r end)*}
+(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}.
 @{ML_response_fake [display,gray]
 "WrongRefData.get @{theory}"
 \end{readmore}
 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
 val ctxt0 = @{context}
 val ctxt1 = ctxt0 |> update @{term \"False\"}
 Move elsewhere
 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
+\<open>foo\<close>. For example you can declare three lemmas to be a member of the
-theorem list @{text foo} by:
+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"}\\
+\isacommand{thm}~\<open>foo\<close>\\
-@{text "> ?C"}\\
+\<open>> ?C\<close>\\
-@{text "> ?B"}
+\<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}:
 @{ML_response_fake [display,gray]
 "FooRules.get @{context}"
 \end{readmore}
 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
+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
-ival} containing an integer and @{text sval} 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
 @{ML_response [display,gray]
 "Config.get @{context} bval"
 "(\"some string\", \"foo\", \"bar\")"}
 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
 shows "(False \<or> True) \<and> True"
 proof (rule conjI)
 show "False \<or> True" using [[simp_trace = true]] by simp
 next
 show "True" by simp
 qed
-text {*
+text \<open>
 in order to inspect how the simplifier solves the first subgoal.
 \begin{readmore}
 For more information about configuration values see
 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
 statically to entities from the logic level of Isabelle. Isabelle also
 contains mechanisms for storing arbitrary data in theory and proof
 \item Print messages that belong together in a single string.
 \item Do not use references in Isabelle code.
 \end{itemize}
 \end{conventions}
-*}
+\<close>
 end

changeset 565	cecd7a941885
parent 564	6e2479089226
child 566	6103b0eadbf2