isabelle-cookbook: comparison ProgTutorial/First

equal deleted inserted replaced

-:be23597e81db
+:f875a25aa72d
 \isacommand{ML}-command. For example:
 \begin{isabelle}
 \begin{graybox}
 \isacommand{ML}~\<open>\<verbopen>\<close>\isanewline
-\hspace{5mm}@{ML "3 + 4"}\isanewline
+\hspace{5mm}@{ML \<open>3 + 4\<close>}\isanewline
 \<open>\<verbclose>\<close>\isanewline
 \<open>> 7\<close>\smallskip
 \end{graybox}
 \end{isabelle}
 \begin{quote}
 \begin{isabelle}
 \isacommand{lemma}~\<open>test:\<close>\isanewline
 \isacommand{shows}~@{text [quotes] "True"}\isanewline
-\isacommand{ML\_prf}~\<open>\<verbopen>\<close>~@{ML "writeln \"Trivial!\""}~\<open>\<verbclose>\<close>\isanewline
+\isacommand{ML\_prf}~\<open>\<verbopen>\<close>~@{ML \<open>writeln "Trivial!"\<close>}~\<open>\<verbclose>\<close>\isanewline
 \isacommand{oops}
 \end{isabelle}
 \end{quote}
 However, both commands will only play minor roles in this tutorial (we most of
 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_matchresult_fake [display,gray] "writeln \"any string\"" "\"any string\""}
+@{ML_matchresult_fake [display,gray] \<open>writeln "any string"\<close> \<open>"any string"\<close>}
 will print out @{text [quotes] "any string"}.
 This function expects a string as argument. If you develop under
 PolyML, then there is a convenient, though again ``quick-and-dirty'', method
 for converting values into strings, namely the antiquotation
 You can print out error messages with the function @{ML_ind error in Library};
 for example:
 @{ML_matchresult_fake [display,gray]
-"if 0 = 1 then true else (error \"foo\")"
+\<open>if 0 = 1 then true else (error "foo")\<close>
-"*** foo
+\<open>*** foo
-***"}
+***\<close>}
 This function raises the exception \<open>ERROR\<close>, which will then
 be displayed by the infrastructure indicating that it is an error by
 painting the output red. Note that this exception is meant
 for ``user-level'' error messages seen by the ``end-user''.
 text \<open>
 They can be used as follows
 @{ML_matchresult_fake [display,gray]
-"pwriteln (pretty_term @{context} @{term \"1::nat\"})"
+\<open>pwriteln (pretty_term @{context} @{term "1::nat"})\<close>
-"\"1\""}
+\<open>"1"\<close>}
 If there is more than one term to be printed, you can use the
 function @{ML_ind commas in Pretty} and @{ML_ind block in Pretty}
 to separate them.
 \<close>
 text \<open>
 Now by using this context @{ML pretty_term} prints out
 @{ML_matchresult_fake [display, gray]
-"pwriteln (pretty_term show_types_ctxt @{term \"(1::nat, x)\"})"
+\<open>pwriteln (pretty_term show_types_ctxt @{term "(1::nat, x)"})\<close>
-"(1::nat, x::'a)"}
+\<open>(1::nat, x::'a)\<close>}
 where \<open>1\<close> and \<open>x\<close> are displayed with their inferred types.
 Other configuration values that influence
 printing of terms include
 For example, the theorem
 @{thm [source] conjI} shown below can be used for any (typable)
 instantiation of \<open>?P\<close> and \<open>?Q\<close>.
 @{ML_matchresult_fake [display, gray]
-"pwriteln (pretty_thm @{context} @{thm conjI})"
+\<open>pwriteln (pretty_thm @{context} @{thm conjI})\<close>
-"\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q"}
+\<open>\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q\<close>}
 However, to improve the readability when printing theorems, we
 can switch off the question marks as follows:
 \<close>
 text \<open>
 With this function, theorem @{thm [source] conjI} is now printed as follows:
 @{ML_matchresult_fake [display, gray]
-"pwriteln (pretty_thm_no_vars @{context} @{thm conjI})"
+\<open>pwriteln (pretty_thm_no_vars @{context} @{thm conjI})\<close>
-"\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> P \<and> Q"}
+\<open>\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> P \<and> Q\<close>}
 Again the functions @{ML commas} and @{ML block in Pretty} help
 with printing more than one theorem.
 \<close>
 together, like a warning message consisting of a term and its type, you
 should try to print these parcels together in a single string. Therefore do
 \emph{not} print out information as
 @{ML_matchresult_fake [display,gray]
-"pwriteln (Pretty.str \"First half,\");
+\<open>pwriteln (Pretty.str "First half,");
-pwriteln (Pretty.str \"and second half.\")"
+pwriteln (Pretty.str "and second half.")\<close>
-"First half,
+\<open>First half,
-and second half."}
+and second half.\<close>}
 but as a single string with appropriate formatting. For example
 @{ML_matchresult_fake [display,gray]
-"pwriteln (Pretty.str (\"First half,\" ^ \"\\n\" ^ \"and second half.\"))"
+\<open>pwriteln (Pretty.str ("First half," ^ "\\n" ^ "and second half."))\<close>
-"First half,
+\<open>First half,
-and second half."}
+and second half.\<close>}
 To ease this kind of string manipulations, there are a number
 of library functions in Isabelle. For example,  the function
 @{ML_ind cat_lines in Library} concatenates a list of strings
 and inserts newlines in between each element.
 @{ML_matchresult_fake [display, gray]
-"pwriteln (Pretty.str (cat_lines [\"foo\", \"bar\"]))"
+\<open>pwriteln (Pretty.str (cat_lines ["foo", "bar"]))\<close>
-"foo
+\<open>foo
-bar"}
+bar\<close>}
 Section \ref{sec:pretty} will explain the infrastructure that Isabelle
 provides for more elaborate pretty printing.
 \begin{readmore}
 |> map Free
 |> curry list_comb f\<close>
 text \<open>
 This function takes a term and a context as arguments. If the term is of function
-type, then @{ML "apply_fresh_args"} returns the term with distinct variables
+type, then @{ML \<open>apply_fresh_args\<close>} returns the term with distinct variables
 applied to it. For example, below three variables are applied to the term
 @{term [show_types] "P::nat \<Rightarrow> int \<Rightarrow> unit \<Rightarrow> bool"}:
 @{ML_matchresult_fake [display,gray]
-"let
+\<open>let
-val trm = @{term \"P::nat \<Rightarrow> int \<Rightarrow> unit \<Rightarrow> bool\"}
+val trm = @{term "P::nat \<Rightarrow> int \<Rightarrow> unit \<Rightarrow> bool"}
 val ctxt = @{context}
 in
 apply_fresh_args trm ctxt
 |> pretty_term ctxt
 |> pwriteln
-end"
+end\<close>
-"P z za zb"}
+\<open>P z za zb\<close>}
 You can read off this behaviour from how @{ML apply_fresh_args} is coded: in
 Line 2, the function @{ML_ind fastype_of in Term} calculates the type of the
 term; @{ML_ind binder_types in Term} in the next line produces the list of
 argument types (in the case above the list \<open>[nat, int, unit]\<close>); Line
 Functions like @{ML apply_fresh_args} are often needed when constructing
 terms involving fresh variables. For this the infrastructure helps
 tremendously to avoid any name clashes. Consider for example:
 @{ML_matchresult_fake [display,gray]
-"let
+\<open>let
-val trm = @{term \"za::'a \<Rightarrow> 'b \<Rightarrow> 'c\"}
+val trm = @{term "za::'a \<Rightarrow> 'b \<Rightarrow> 'c"}
 val ctxt = @{context}
 in
 apply_fresh_args trm ctxt
 |> pretty_term ctxt
 |> pwriteln
-end"
+end\<close>
-"za z zb"}
+\<open>za z zb\<close>}
 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
 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,
+can be composed with @{ML \<open>#>\<close>}. Consider for example the following code,
 where we store the theorems @{thm [source] conjI}, @{thm [source] conjunct1}
 and @{thm [source] conjunct2} under alternative names.
 \<close>
 local_setup %graylinenos \<open>
 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_structure Local_Theory};
 it stores a theorem under a name.
 In lines 5 to 6 we call this function to give alternative names for the three
-theorems. The point of @{ML "#>"} is that you can sequence such function calls.
+theorems. The point of @{ML \<open>#>\<close>} is that you can sequence such function calls.
 The remaining combinators we describe in this section add convenience for
 the ``waterfall method'' of writing functions. The combinator @{ML_ind tap
 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
 x |> `(fn x => x + 1)
 |> (fn (x, y) => (x, y + 1))\<close>
 text \<open>
 which takes \<open>x\<close> as argument, and then increments \<open>x\<close>, but also keeps
-\<open>x\<close>. The intermediate result is therefore the pair @{ML "(x + 1, x)"
+\<open>x\<close>. The intermediate result is therefore the pair @{ML \<open>(x + 1, x)\<close>
 for x}. After that, the function increments the right-hand component of the
-pair. So finally the result will be @{ML "(x + 1, x + 1)" for x}.
+pair. So finally the result will be @{ML \<open>(x + 1, x + 1)\<close> for x}.
 The combinators @{ML_ind "|>>" in Basics} and @{ML_ind "||>" in Basics} are
 defined for functions manipulating pairs. The first applies the function to
 the first component of the pair, defined as
 \<close>
 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]"}
+threshold. If the threshold is @{ML \<open>5\<close>}, the list @{ML \<open>[1,6,2,5,3,4]\<close>}
-should be separated as @{ML "([1,2,3,4], [6,5])"}.  Such a function can be
+should be separated as @{ML \<open>([1,2,3,4], [6,5])\<close>}.  Such a function can be
 implemented as
 \<close>
 ML %grayML\<open>fun separate i [] = ([], [])
 | separate i (x::xs) =
 if i <= x then (los, x::grs) else (x::los, grs)
 end\<close>
 text \<open>
 where the return value of the recursive call is bound explicitly to
-the pair @{ML "(los, grs)" for los grs}. However, this function
+the pair @{ML \<open>(los, grs)\<close> for los grs}. However, this function
 can be implemented more concisely as
 \<close>
 ML %grayML\<open>fun separate _ [] = ([], [])
 | separate i (x::xs) =
 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_matchresult [display,gray]
-"acc_incs 1"
+\<open>acc_incs 1\<close>
-"((((\"\", 1), 2), 3), 4)"}
+\<open>(((("", 1), 2), 3), 4)\<close>}
 You can continue this chain with:
 @{ML_matchresult [display,gray]
-"acc_incs 1 ||>> (fn x => (x, x + 2))"
+\<open>acc_incs 1 ||>> (fn x => (x, x + 2))\<close>
-"(((((\"\", 1), 2), 3), 4), 6)"}
+\<open>((((("", 1), 2), 3), 4), 6)\<close>}
 An example where this combinator is useful is as follows
 @{ML_matchresult_fake [display, gray]
-"let
+\<open>let
 val ((names1, names2), _) =
 @{context}
-|> Variable.variant_fixes (replicate 4 \"x\")
+|> Variable.variant_fixes (replicate 4 "x")
-||>> Variable.variant_fixes (replicate 5 \"x\")
+||>> Variable.variant_fixes (replicate 5 "x")
 in
 (names1, names2)
-end"
+end\<close>
-"([\"x\", \"xa\", \"xb\", \"xc\"], [\"xd\", \"xe\", \"xf\", \"xg\", \"xh\"])"}
+\<open>(["x", "xa", "xb", "xc"], ["xd", "xe", "xf", "xg", "xh"])\<close>}
-Its purpose is to create nine variants of the string @{ML "\"x\""} so
+Its purpose is to create nine variants of the string @{ML \<open>"x"\<close>} so
 that no variant will clash with another. Suppose for some reason we want
 to bind four variants to the lists @{ML_text "name1"} and the
 rest to @{ML_text "name2"}. In order to obtain non-clashing
 variants we have to thread the context through the function calls
 (the context records which variants have been previously created).
-For the first call we can use @{ML "|>"}, but in the
+For the first call we can use @{ML \<open>|>\<close>}, but in the
 second and any further call to @{ML_ind variant_fixes in Variable} we
-have to use @{ML "||>>"} in order to account for the result(s)
+have to use @{ML \<open>||>>\<close>} in order to account for the result(s)
 obtained by previous calls.
 A more realistic example for this combinator is the following code
 \<close>
 information about the definitions---the function @{ML_ind define in Local_Defs} returns
 both as pairs. We can use this information for example to print out the definiens and
 the theorem corresponding to the definitions. For example for the first definition:
 @{ML_matchresult_fake [display, gray]
-"let
+\<open>let
 val (one_trm, (_, one_thm)) = one_def
 in
 pwriteln (pretty_term ctxt' one_trm);
 pwriteln (pretty_thm ctxt' one_thm)
-end"
+end\<close>
-"One
+\<open>One
-One \<equiv> 1"}
+One \<equiv> 1\<close>}
-Recall that @{ML "|>"} is the reverse function application. Recall also that
+Recall that @{ML \<open>|>\<close>} is the reverse function application. Recall also that
-the related reverse function composition is @{ML "#>"}. In fact all the
+the related reverse function composition is @{ML \<open>#>\<close>}. In fact all the
-combinators @{ML "|->"}, @{ML "|>>"} , @{ML "||>"} and @{ML "||>>"}
+combinators @{ML \<open>|->\<close>}, @{ML \<open>|>>\<close>} , @{ML \<open>||>\<close>} and @{ML \<open>||>>\<close>}
 described above have related combinators for function composition, namely
 @{ML_ind "#->" in Basics}, @{ML_ind "#>>" in Basics}, @{ML_ind "##>" in
-Basics} and @{ML_ind "##>>" in Basics}. Using @{ML "#->"}, for example, the
+Basics} and @{ML_ind "##>>" in Basics}. Using @{ML \<open>#->\<close>}, for example, the
 function \<open>double\<close> can also be written as:
 \<close>
 ML %grayML\<open>val double =
 (fn x => (x, x)) #->
 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
+list_comb}, which works over pairs, to fit with the combinator @{ML \<open>|>\<close>}. Such
 plumbing is also needed in situations where a function operates over lists,
 but one calculates only with a single element. An example is the function
 @{ML_ind check_terms in Syntax}, whose purpose is to simultaneously type-check
 a list of terms. Consider the code:
 @{ML_matchresult_fake [display, gray]
-"let
+\<open>let
 val ctxt = @{context}
 in
-map (Syntax.parse_term ctxt) [\"m + n\", \"m * n\", \"m - (n::nat)\"]
+map (Syntax.parse_term ctxt) ["m + n", "m * n", "m - (n::nat)"]
 |> Syntax.check_terms ctxt
 |> pretty_terms ctxt
 |> pwriteln
-end"
+end\<close>
-"m + n, m * n, m - n"}
+\<open>m + n, m * n, m - n\<close>}
 \<close>
 text \<open>
 In this example we obtain three terms (using the function
 @{ML_ind parse_term in Syntax}) whose variables \<open>m\<close> and \<open>n\<close>
 @{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
 @{ML_matchresult_fake [display, gray, linenos]
-"let
+\<open>let
 val ctxt = @{context}
 in
-Syntax.parse_term ctxt \"m - (n::nat)\"
+Syntax.parse_term ctxt "m - (n::nat)"
 |> singleton (Syntax.check_terms ctxt)
 |> pretty_term ctxt
 |> pwriteln
-end"
+end\<close>
-"m - n"}
+\<open>m - n\<close>}
 where in Line 5, the function operating over lists fits with the
 single term generated in Line 4.
 \begin{readmore}
 and @{ML_file "Pure/General/basics.ML"}. Also \isccite{sec:ML-linear-trans}
 contains further information about combinators.
 \end{readmore}
 \begin{exercise}
-Find out what the combinator @{ML "K I"} does.
+Find out what the combinator @{ML \<open>K I\<close>} does.
 \end{exercise}
 \<close>
 section \<open>ML-Antiquotations\label{sec:antiquote}\<close>
 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 \<open>{\<dots>}\<close>.  For example, one can print out the name of the current theory with
 the code
-@{ML_matchresult [display,gray] "Context.theory_name @{theory}" "\"First_Steps\""}
+@{ML_matchresult [display,gray] \<open>Context.theory_name @{theory}\<close> \<open>"First_Steps"\<close>}
 where \<open>@{theory}\<close> is an antiquotation that is substituted with the
 current theory (remember that we assumed we are inside the theory
 \<open>First_Steps\<close>). The name of this theory can be extracted using
 the function @{ML_ind theory_name in Context}.
 \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
 @{ML_matchresult_fake [display, gray]
-"Proof_Context.print_abbrevs false @{context}"
+\<open>Proof_Context.print_abbrevs false @{context}\<close>
-"\<dots>
+\<open>\<dots>
 INTER \<equiv> INFI
 Inter \<equiv> Inf
-\<dots>"}
+\<dots>\<close>}
 The precise output of course depends on the abbreviations that are
 currently defined; this can change over time.
 You can also use antiquotations to refer to proved theorems:
 \<open>@{thm \<dots>}\<close> for a single theorem
-@{ML_matchresult_fake [display,gray] "@{thm allI}" "(\<And>x. ?P x) \<Longrightarrow> \<forall>x. ?P x"}
+@{ML_matchresult_fake [display,gray] \<open>@{thm allI}\<close> \<open>(\<And>x. ?P x) \<Longrightarrow> \<forall>x. ?P x\<close>}
 and \<open>@{thms \<dots>}\<close> for more than one
 @{ML_matchresult_fake [display,gray]
-"@{thms conj_ac}"
+\<open>@{thms conj_ac}\<close>
-"(?P \<and> ?Q) = (?Q \<and> ?P)
+\<open>(?P \<and> ?Q) = (?Q \<and> ?P)
 (?P \<and> ?Q \<and> ?R) = (?Q \<and> ?P \<and> ?R)
-((?P \<and> ?Q) \<and> ?R) = (?P \<and> ?Q \<and> ?R)"}
+((?P \<and> ?Q) \<and> ?R) = (?P \<and> ?Q \<and> ?R)\<close>}
 The thm-antiquotations can also be used for manipulating theorems. For
 example, if you need the version of the theorem @{thm [source] refl} that
 has a meta-equality instead of an equality, you can write
 @{ML_matchresult_fake [display,gray]
-"@{thm refl[THEN eq_reflection]}"
+\<open>@{thm refl[THEN eq_reflection]}\<close>
-"?x \<equiv> ?x"}
+\<open>?x \<equiv> ?x\<close>}
 The point of these antiquotations is that referring to theorems in this way
 makes your code independent from what theorems the user might have stored
 under this name (this becomes especially important when you deal with
 theorem lists; see Section \ref{sec:storing}).
 text \<open>
 The result can be printed out as follows.
 @{ML_matchresult_fake [gray,display]
-"foo_thms |> pretty_thms_no_vars @{context}
+\<open>foo_thms |> pretty_thms_no_vars @{context}
-|> pwriteln"
+|> pwriteln\<close>
-"True, False \<Longrightarrow> P"}
+\<open>True, False \<Longrightarrow> P\<close>}
 You can also refer to the current simpset via an antiquotation. To illustrate
 this we implement the function that extracts the theorem names stored in a
 simpset.
 \<close>
 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}.
 @{ML_matchresult_fake [display,gray]
-"get_thm_names_from_ss @{context}"
+\<open>get_thm_names_from_ss @{context}\<close>
-"[\"Nat.of_nat_eq_id\", \"Int.of_int_eq_id\", \"Nat.One_nat_def\", \<dots>]"}
+\<open>["Nat.of_nat_eq_id", "Int.of_int_eq_id", "Nat.One_nat_def", \<dots>]\<close>}
 Again, this way of referencing simpsets makes you independent from additions
 of lemmas to the simpset by the user, which can potentially cause loops in your
 code.
 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_matchresult_fake [display,gray]
-"@{term_pat \"Suc (?x::nat)\"}"
+\<open>@{term_pat "Suc (?x::nat)"}\<close>
-"Const (\"Suc\", \"nat \<Rightarrow> nat\") $ Var ((\"x\", 0), \"nat\")"}
+\<open>Const ("Suc", "nat \<Rightarrow> nat") $ Var (("x", 0), "nat")\<close>}
 which shows the internal representation of the term \<open>Suc ?x\<close>. Similarly
 we can write an antiquotation for type patterns. Its code is
 \<close>
 text \<open>
 The data can be retrieved with the projection functions defined above.
 @{ML_matchresult_fake [display, gray]
-"project_int (nth foo_list 0);
+\<open>project_int (nth foo_list 0);
-project_bool (nth foo_list 1)"
+project_bool (nth foo_list 1)\<close>
-"13
+\<open>13
-true"}
+true\<close>}
 Notice that we access the integer as an integer and the boolean as
 a boolean. If we attempt to access the integer as a boolean, then we get
 a runtime error.
 @{ML_matchresult_fake [display, gray]
-"project_bool (nth foo_list 0)"
+\<open>project_bool (nth foo_list 0)\<close>
-"*** exception Match raised"}
+\<open>*** exception Match raised\<close>}
 This runtime error is the reason why ML is still type-sound despite
 containing a universal type.
 Now, Isabelle heavily uses this mechanism for storing all sorts of
 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_matchresult_fake [display, gray]
-"lookup @{theory} \"conj\""
+\<open>lookup @{theory} "conj"\<close>
-"SOME \"\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q\""}
+\<open>SOME "\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q"\<close>}
 An important point to note is that these tables (and data in general)
 need to be treated in a purely functional fashion. Although
 we can update the table as follows
 \<close>
 text \<open>
 and accordingly, @{ML lookup} now produces the introduction rule for @{term "True"}
 @{ML_matchresult_fake [display, gray]
-"lookup @{theory} \"conj\""
+\<open>lookup @{theory} "conj"\<close>
-"SOME \"True\""}
+\<open>SOME "True"\<close>}
 there are no references involved. This is one of the most fundamental
 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
 val extend = I
 val merge = fst)\<close>
 text \<open>
 We initialise the reference with the empty list. Consequently a first
-lookup produces @{ML "ref []" in Unsynchronized}.
+lookup produces @{ML \<open>ref []\<close> in Unsynchronized}.
 @{ML_matchresult_fake [display,gray]
-"WrongRefData.get @{theory}"
+\<open>WrongRefData.get @{theory}\<close>
-"ref []"}
+\<open>ref []\<close>}
 For updating the reference we use the following function
 \<close>
 ML %grayML\<open>fun ref_update n = WrongRefData.map
 setup %gray \<open>ref_update 1\<close>
 text \<open>
 A lookup in the current theory gives then the expected list
-@{ML "ref [1]" in Unsynchronized}.
+@{ML \<open>ref [1]\<close> in Unsynchronized}.
 @{ML_matchresult_fake [display,gray]
-"WrongRefData.get @{theory}"
+\<open>WrongRefData.get @{theory}\<close>
-"ref [1]"}
+\<open>ref [1]\<close>}
 So far everything is as expected. But, the trouble starts if we attempt to
 backtrack to the ``point'' before the \isacommand{setup}-command. There, we
 would expect that the list is empty again. But since it is stored in a
 reference, Isabelle has no control over it. So it is not empty, but still
-@{ML "ref [1]" in Unsynchronized}. Adding to the trouble, if we execute the
+@{ML \<open>ref [1]\<close> in Unsynchronized}. Adding to the trouble, if we execute the
-\isacommand{setup}-command again, we do not obtain @{ML "ref [1]" in
+\isacommand{setup}-command again, we do not obtain @{ML \<open>ref [1]\<close> in
 Unsynchronized}, but
 @{ML_matchresult_fake [display,gray]
-"WrongRefData.get @{theory}"
+\<open>WrongRefData.get @{theory}\<close>
-"ref [1, 1]"}
+\<open>ref [1, 1]\<close>}
 Now imagine how often you go backwards and forwards in your proof
 scripts.\footnote{The same problem can be triggered in the Jedit GUI by
 making the parser to go over and over again over the \isacommand{setup} command.}
 By using references in Isabelle code, you are bound to cause all
 text \<open>
 Next we start with the context generated by the antiquotation
 \<open>@{context}\<close> and update it in various ways.
 @{ML_matchresult_fake [display,gray]
-"let
+\<open>let
 val ctxt0 = @{context}
-val ctxt1 = ctxt0 |> update @{term \"False\"}
+val ctxt1 = ctxt0 |> update @{term "False"}
-|> update @{term \"True \<and> True\"}
+|> update @{term "True \<and> True"}
-val ctxt2 = ctxt0 |> update @{term \"1::nat\"}
+val ctxt2 = ctxt0 |> update @{term "1::nat"}
-val ctxt3 = ctxt2 |> update @{term \"2::nat\"}
+val ctxt3 = ctxt2 |> update @{term "2::nat"}
 in
 print ctxt0;
 print ctxt1;
 print ctxt2;
 print ctxt3
-end"
+end\<close>
-"Empty!
+\<open>Empty!
 True \<and> True, False
 1
-2, 1"}
+2, 1\<close>}
 Many functions in Isabelle manage and update data in a similar
 fashion. Consequently, such calculations with contexts occur frequently in
 Isabelle code, although the ``context flow'' is usually only linear.
 Note also that the calculation above has no effect on the underlying
 text \<open>
 The rules in the list can be retrieved using the function
 @{ML FooRules.get}:
 @{ML_matchresult_fake [display,gray]
-"FooRules.get @{context}"
+\<open>FooRules.get @{context}\<close>
-"[\"True\", \"?C\",\"?B\"]"}
+\<open>["True", "?C","?B"]\<close>}
 Note that this function takes a proof context as argument. This might be
 confusing, since the theorem list is stored as theory data. It becomes clear by knowing
 that the proof context contains the information about the current theory and so the function
 can access the theorem list in the theory via the context.
 text \<open>
 On the ML-level these values can be retrieved using the
 function @{ML_ind get in Config} from a proof context
 @{ML_matchresult [display,gray]
-"Config.get @{context} bval"
+\<open>Config.get @{context} bval\<close>
-"true"}
+\<open>true\<close>}
 or directly from a theory using the function @{ML_ind get_global in Config}
 @{ML_matchresult [display,gray]
-"Config.get_global @{theory} bval"
+\<open>Config.get_global @{theory} bval\<close>
-"true"}
+\<open>true\<close>}
 It is also possible to manipulate the configuration values
 from the ML-level with the functions @{ML_ind put in Config}
 and @{ML_ind put_global in Config}. For example
 @{ML_matchresult [display,gray]
-"let
+\<open>let
 val ctxt = @{context}
-val ctxt' = Config.put sval \"foo\" ctxt
+val ctxt' = Config.put sval "foo" ctxt
-val ctxt'' = Config.put sval \"bar\" ctxt'
+val ctxt'' = Config.put sval "bar" ctxt'
 in
 (Config.get ctxt sval,
 Config.get ctxt' sval,
 Config.get ctxt'' sval)
-end"
+end\<close>
-"(\"some string\", \"foo\", \"bar\")"}
+\<open>("some string", "foo", "bar")\<close>}
 A concrete example for a configuration value is
 @{ML_ind simp_trace in Raw_Simplifier}, which switches on trace information
 in the simplifier. This can be used for example in the following proof
 \<close>

changeset 569	f875a25aa72d
parent 567	f7c97e64cc2a
child 572	438703674711