--- a/ProgTutorial/First_Steps.thy Fri May 17 07:29:51 2019 +0200
+++ b/ProgTutorial/First_Steps.thy Fri May 17 10:38:01 2019 +0200
@@ -39,7 +39,7 @@
\begin{isabelle}
\begin{graybox}
\isacommand{ML}~\<open>\<verbopen>\<close>\isanewline
- \hspace{5mm}@{ML "3 + 4"}\isanewline
+ \hspace{5mm}@{ML \<open>3 + 4\<close>}\isanewline
\<open>\<verbclose>\<close>\isanewline
\<open>> 7\<close>\smallskip
\end{graybox}
@@ -61,7 +61,7 @@
\begin{isabelle}
\isacommand{lemma}~\<open>test:\<close>\isanewline
\isacommand{shows}~@{text [quotes] "True"}\isanewline
- \isacommand{ML\_prf}~\<open>\<verbopen>\<close>~@{ML "writeln \"Trivial!\""}~\<open>\<verbclose>\<close>\isanewline
+ \isacommand{ML\_prf}~\<open>\<verbopen>\<close>~@{ML \<open>writeln "Trivial!"\<close>}~\<open>\<verbclose>\<close>\isanewline
\isacommand{oops}
\end{isabelle}
\end{quote}
@@ -93,7 +93,7 @@
code. This can be done in a ``quick-and-dirty'' fashion using the function
@{ML_ind writeln in Output}. For example
- @{ML_matchresult_fake [display,gray] "writeln \"any string\"" "\"any string\""}
+ @{ML_matchresult_fake [display,gray] \<open>writeln "any string"\<close> \<open>"any string"\<close>}
will print out @{text [quotes] "any string"}.
This function expects a string as argument. If you develop under
@@ -110,9 +110,9 @@
for example:
@{ML_matchresult_fake [display,gray]
- "if 0 = 1 then true else (error \"foo\")"
-"*** foo
-***"}
+ \<open>if 0 = 1 then true else (error "foo")\<close>
+\<open>*** foo
+***\<close>}
This function raises the exception \<open>ERROR\<close>, which will then
be displayed by the infrastructure indicating that it is an error by
@@ -137,8 +137,8 @@
They can be used as follows
@{ML_matchresult_fake [display,gray]
- "pwriteln (pretty_term @{context} @{term \"1::nat\"})"
- "\"1\""}
+ \<open>pwriteln (pretty_term @{context} @{term "1::nat"})\<close>
+ \<open>"1"\<close>}
If there is more than one term to be printed, you can use the
function @{ML_ind commas in Pretty} and @{ML_ind block in Pretty}
@@ -160,8 +160,8 @@
Now by using this context @{ML pretty_term} prints out
@{ML_matchresult_fake [display, gray]
- "pwriteln (pretty_term show_types_ctxt @{term \"(1::nat, x)\"})"
- "(1::nat, x::'a)"}
+ \<open>pwriteln (pretty_term show_types_ctxt @{term "(1::nat, x)"})\<close>
+ \<open>(1::nat, x::'a)\<close>}
where \<open>1\<close> and \<open>x\<close> are displayed with their inferred types.
Other configuration values that influence
@@ -204,8 +204,8 @@
instantiation of \<open>?P\<close> and \<open>?Q\<close>.
@{ML_matchresult_fake [display, gray]
- "pwriteln (pretty_thm @{context} @{thm conjI})"
- "\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q"}
+ \<open>pwriteln (pretty_thm @{context} @{thm conjI})\<close>
+ \<open>\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q\<close>}
However, to improve the readability when printing theorems, we
can switch off the question marks as follows:
@@ -222,8 +222,8 @@
With this function, theorem @{thm [source] conjI} is now printed as follows:
@{ML_matchresult_fake [display, gray]
- "pwriteln (pretty_thm_no_vars @{context} @{thm conjI})"
- "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> P \<and> Q"}
+ \<open>pwriteln (pretty_thm_no_vars @{context} @{thm conjI})\<close>
+ \<open>\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> P \<and> Q\<close>}
Again the functions @{ML commas} and @{ML block in Pretty} help
with printing more than one theorem.
@@ -265,17 +265,17 @@
\emph{not} print out information as
@{ML_matchresult_fake [display,gray]
-"pwriteln (Pretty.str \"First half,\");
-pwriteln (Pretty.str \"and second half.\")"
-"First half,
-and second half."}
+\<open>pwriteln (Pretty.str "First half,");
+pwriteln (Pretty.str "and second half.")\<close>
+\<open>First half,
+and second half.\<close>}
but as a single string with appropriate formatting. For example
@{ML_matchresult_fake [display,gray]
-"pwriteln (Pretty.str (\"First half,\" ^ \"\\n\" ^ \"and second half.\"))"
-"First half,
-and second half."}
+\<open>pwriteln (Pretty.str ("First half," ^ "\\n" ^ "and second half."))\<close>
+\<open>First half,
+and second half.\<close>}
To ease this kind of string manipulations, there are a number
of library functions in Isabelle. For example, the function
@@ -283,9 +283,9 @@
and inserts newlines in between each element.
@{ML_matchresult_fake [display, gray]
- "pwriteln (Pretty.str (cat_lines [\"foo\", \"bar\"]))"
- "foo
-bar"}
+ \<open>pwriteln (Pretty.str (cat_lines ["foo", "bar"]))\<close>
+ \<open>foo
+bar\<close>}
Section \ref{sec:pretty} will explain the infrastructure that Isabelle
provides for more elaborate pretty printing.
@@ -383,20 +383,20 @@
text \<open>
This function takes a term and a context as arguments. If the term is of function
- type, then @{ML "apply_fresh_args"} returns the term with distinct variables
+ type, then @{ML \<open>apply_fresh_args\<close>} returns the term with distinct variables
applied to it. For example, below three variables are applied to the term
@{term [show_types] "P::nat \<Rightarrow> int \<Rightarrow> unit \<Rightarrow> bool"}:
@{ML_matchresult_fake [display,gray]
-"let
- val trm = @{term \"P::nat \<Rightarrow> int \<Rightarrow> unit \<Rightarrow> bool\"}
+\<open>let
+ val trm = @{term "P::nat \<Rightarrow> int \<Rightarrow> unit \<Rightarrow> bool"}
val ctxt = @{context}
in
apply_fresh_args trm ctxt
|> pretty_term ctxt
|> pwriteln
-end"
- "P z za zb"}
+end\<close>
+ \<open>P z za zb\<close>}
You can read off this behaviour from how @{ML apply_fresh_args} is coded: in
Line 2, the function @{ML_ind fastype_of in Term} calculates the type of the
@@ -415,15 +415,15 @@
tremendously to avoid any name clashes. Consider for example:
@{ML_matchresult_fake [display,gray]
-"let
- val trm = @{term \"za::'a \<Rightarrow> 'b \<Rightarrow> 'c\"}
+\<open>let
+ val trm = @{term "za::'a \<Rightarrow> 'b \<Rightarrow> 'c"}
val ctxt = @{context}
in
apply_fresh_args trm ctxt
|> pretty_term ctxt
|> pwriteln
-end"
- "za z zb"}
+end\<close>
+ \<open>za z zb\<close>}
where the \<open>za\<close> is correctly avoided.
@@ -444,7 +444,7 @@
\isacommand{setup}- or \isacommand{local\_setup}-command. These functions
have to be of type @{ML_type "theory -> theory"}, respectively
@{ML_type "local_theory -> local_theory"}. More than one such setup function
- can be composed with @{ML "#>"}. Consider for example the following code,
+ can be composed with @{ML \<open>#>\<close>}. Consider for example the following code,
where we store the theorems @{thm [source] conjI}, @{thm [source] conjunct1}
and @{thm [source] conjunct2} under alternative names.
\<close>
@@ -463,7 +463,7 @@
@{ML_ind note in Local_Theory} in the structure @{ML_structure Local_Theory};
it stores a theorem under a name.
In lines 5 to 6 we call this function to give alternative names for the three
- theorems. The point of @{ML "#>"} is that you can sequence such function calls.
+ theorems. The point of @{ML \<open>#>\<close>} is that you can sequence such function calls.
The remaining combinators we describe in this section add convenience for
the ``waterfall method'' of writing functions. The combinator @{ML_ind tap
@@ -501,9 +501,9 @@
text \<open>
which takes \<open>x\<close> as argument, and then increments \<open>x\<close>, but also keeps
- \<open>x\<close>. The intermediate result is therefore the pair @{ML "(x + 1, x)"
+ \<open>x\<close>. The intermediate result is therefore the pair @{ML \<open>(x + 1, x)\<close>
for x}. After that, the function increments the right-hand component of the
- pair. So finally the result will be @{ML "(x + 1, x + 1)" for x}.
+ pair. So finally the result will be @{ML \<open>(x + 1, x + 1)\<close> for x}.
The combinators @{ML_ind "|>>" in Basics} and @{ML_ind "||>" in Basics} are
defined for functions manipulating pairs. The first applies the function to
@@ -522,8 +522,8 @@
These two functions can, for example, be used to avoid explicit \<open>lets\<close> for
intermediate values in functions that return pairs. As an example, suppose you
want to separate a list of integers into two lists according to a
- threshold. If the threshold is @{ML "5"}, the list @{ML "[1,6,2,5,3,4]"}
- should be separated as @{ML "([1,2,3,4], [6,5])"}. Such a function can be
+ threshold. If the threshold is @{ML \<open>5\<close>}, the list @{ML \<open>[1,6,2,5,3,4]\<close>}
+ should be separated as @{ML \<open>([1,2,3,4], [6,5])\<close>}. Such a function can be
implemented as
\<close>
@@ -537,7 +537,7 @@
text \<open>
where the return value of the recursive call is bound explicitly to
- the pair @{ML "(los, grs)" for los grs}. However, this function
+ the pair @{ML \<open>(los, grs)\<close> for los grs}. However, this function
can be implemented more concisely as
\<close>
@@ -588,37 +588,37 @@
the value by one, but also nest the intermediate results to the left. For example
@{ML_matchresult [display,gray]
- "acc_incs 1"
- "((((\"\", 1), 2), 3), 4)"}
+ \<open>acc_incs 1\<close>
+ \<open>(((("", 1), 2), 3), 4)\<close>}
You can continue this chain with:
@{ML_matchresult [display,gray]
- "acc_incs 1 ||>> (fn x => (x, x + 2))"
- "(((((\"\", 1), 2), 3), 4), 6)"}
+ \<open>acc_incs 1 ||>> (fn x => (x, x + 2))\<close>
+ \<open>((((("", 1), 2), 3), 4), 6)\<close>}
An example where this combinator is useful is as follows
@{ML_matchresult_fake [display, gray]
- "let
+ \<open>let
val ((names1, names2), _) =
@{context}
- |> Variable.variant_fixes (replicate 4 \"x\")
- ||>> Variable.variant_fixes (replicate 5 \"x\")
+ |> Variable.variant_fixes (replicate 4 "x")
+ ||>> Variable.variant_fixes (replicate 5 "x")
in
(names1, names2)
-end"
- "([\"x\", \"xa\", \"xb\", \"xc\"], [\"xd\", \"xe\", \"xf\", \"xg\", \"xh\"])"}
+end\<close>
+ \<open>(["x", "xa", "xb", "xc"], ["xd", "xe", "xf", "xg", "xh"])\<close>}
- Its purpose is to create nine variants of the string @{ML "\"x\""} so
+ Its purpose is to create nine variants of the string @{ML \<open>"x"\<close>} so
that no variant will clash with another. Suppose for some reason we want
to bind four variants to the lists @{ML_text "name1"} and the
rest to @{ML_text "name2"}. In order to obtain non-clashing
variants we have to thread the context through the function calls
(the context records which variants have been previously created).
- For the first call we can use @{ML "|>"}, but in the
+ For the first call we can use @{ML \<open>|>\<close>}, but in the
second and any further call to @{ML_ind variant_fixes in Variable} we
- have to use @{ML "||>>"} in order to account for the result(s)
+ have to use @{ML \<open>||>>\<close>} in order to account for the result(s)
obtained by previous calls.
A more realistic example for this combinator is the following code
@@ -640,20 +640,20 @@
the theorem corresponding to the definitions. For example for the first definition:
@{ML_matchresult_fake [display, gray]
- "let
+ \<open>let
val (one_trm, (_, one_thm)) = one_def
in
pwriteln (pretty_term ctxt' one_trm);
pwriteln (pretty_thm ctxt' one_thm)
-end"
- "One
-One \<equiv> 1"}
- Recall that @{ML "|>"} is the reverse function application. Recall also that
- the related reverse function composition is @{ML "#>"}. In fact all the
- combinators @{ML "|->"}, @{ML "|>>"} , @{ML "||>"} and @{ML "||>>"}
+end\<close>
+ \<open>One
+One \<equiv> 1\<close>}
+ Recall that @{ML \<open>|>\<close>} is the reverse function application. Recall also that
+ the related reverse function composition is @{ML \<open>#>\<close>}. In fact all the
+ combinators @{ML \<open>|->\<close>}, @{ML \<open>|>>\<close>} , @{ML \<open>||>\<close>} and @{ML \<open>||>>\<close>}
described above have related combinators for function composition, namely
@{ML_ind "#->" in Basics}, @{ML_ind "#>>" in Basics}, @{ML_ind "##>" in
- Basics} and @{ML_ind "##>>" in Basics}. Using @{ML "#->"}, for example, the
+ Basics} and @{ML_ind "##>>" in Basics}. Using @{ML \<open>#->\<close>}, for example, the
function \<open>double\<close> can also be written as:
\<close>
@@ -667,22 +667,22 @@
sometimes necessary to do some ``plumbing'' in order to fit functions
together. We have already seen such plumbing in the function @{ML
apply_fresh_args}, where @{ML curry} is needed for making the function @{ML
- list_comb}, which works over pairs, to fit with the combinator @{ML "|>"}. Such
+ list_comb}, which works over pairs, to fit with the combinator @{ML \<open>|>\<close>}. Such
plumbing is also needed in situations where a function operates over lists,
but one calculates only with a single element. An example is the function
@{ML_ind check_terms in Syntax}, whose purpose is to simultaneously type-check
a list of terms. Consider the code:
@{ML_matchresult_fake [display, gray]
- "let
+ \<open>let
val ctxt = @{context}
in
- map (Syntax.parse_term ctxt) [\"m + n\", \"m * n\", \"m - (n::nat)\"]
+ map (Syntax.parse_term ctxt) ["m + n", "m * n", "m - (n::nat)"]
|> Syntax.check_terms ctxt
|> pretty_terms ctxt
|> pwriteln
-end"
- "m + n, m * n, m - n"}
+end\<close>
+ \<open>m + n, m * n, m - n\<close>}
\<close>
text \<open>
@@ -695,15 +695,15 @@
in terms of @{ML singleton} and @{ML check_terms in Syntax}.} For example
@{ML_matchresult_fake [display, gray, linenos]
- "let
+ \<open>let
val ctxt = @{context}
in
- Syntax.parse_term ctxt \"m - (n::nat)\"
+ Syntax.parse_term ctxt "m - (n::nat)"
|> singleton (Syntax.check_terms ctxt)
|> pretty_term ctxt
|> pwriteln
-end"
- "m - n"}
+end\<close>
+ \<open>m - n\<close>}
where in Line 5, the function operating over lists fits with the
single term generated in Line 4.
@@ -716,7 +716,7 @@
\end{readmore}
\begin{exercise}
- Find out what the combinator @{ML "K I"} does.
+ Find out what the combinator @{ML \<open>K I\<close>} does.
\end{exercise}
\<close>
@@ -743,7 +743,7 @@
are indicated by the @{ML_text @}-sign followed by text wrapped in \<open>{\<dots>}\<close>. For example, one can print out the name of the current theory with
the code
- @{ML_matchresult [display,gray] "Context.theory_name @{theory}" "\"First_Steps\""}
+ @{ML_matchresult [display,gray] \<open>Context.theory_name @{theory}\<close> \<open>"First_Steps"\<close>}
where \<open>@{theory}\<close> is an antiquotation that is substituted with the
current theory (remember that we assumed we are inside the theory
@@ -772,34 +772,34 @@
defined abbreviations. For example
@{ML_matchresult_fake [display, gray]
- "Proof_Context.print_abbrevs false @{context}"
-"\<dots>
+ \<open>Proof_Context.print_abbrevs false @{context}\<close>
+\<open>\<dots>
INTER \<equiv> INFI
Inter \<equiv> Inf
-\<dots>"}
+\<dots>\<close>}
The precise output of course depends on the abbreviations that are
currently defined; this can change over time.
You can also use antiquotations to refer to proved theorems:
\<open>@{thm \<dots>}\<close> for a single theorem
- @{ML_matchresult_fake [display,gray] "@{thm allI}" "(\<And>x. ?P x) \<Longrightarrow> \<forall>x. ?P x"}
+ @{ML_matchresult_fake [display,gray] \<open>@{thm allI}\<close> \<open>(\<And>x. ?P x) \<Longrightarrow> \<forall>x. ?P x\<close>}
and \<open>@{thms \<dots>}\<close> for more than one
@{ML_matchresult_fake [display,gray]
- "@{thms conj_ac}"
-"(?P \<and> ?Q) = (?Q \<and> ?P)
+ \<open>@{thms conj_ac}\<close>
+\<open>(?P \<and> ?Q) = (?Q \<and> ?P)
(?P \<and> ?Q \<and> ?R) = (?Q \<and> ?P \<and> ?R)
-((?P \<and> ?Q) \<and> ?R) = (?P \<and> ?Q \<and> ?R)"}
+((?P \<and> ?Q) \<and> ?R) = (?P \<and> ?Q \<and> ?R)\<close>}
The thm-antiquotations can also be used for manipulating theorems. For
example, if you need the version of the theorem @{thm [source] refl} that
has a meta-equality instead of an equality, you can write
@{ML_matchresult_fake [display,gray]
- "@{thm refl[THEN eq_reflection]}"
- "?x \<equiv> ?x"}
+ \<open>@{thm refl[THEN eq_reflection]}\<close>
+ \<open>?x \<equiv> ?x\<close>}
The point of these antiquotations is that referring to theorems in this way
makes your code independent from what theorems the user might have stored
@@ -817,9 +817,9 @@
The result can be printed out as follows.
@{ML_matchresult_fake [gray,display]
-"foo_thms |> pretty_thms_no_vars @{context}
- |> pwriteln"
- "True, False \<Longrightarrow> P"}
+\<open>foo_thms |> pretty_thms_no_vars @{context}
+ |> pwriteln\<close>
+ \<open>True, False \<Longrightarrow> P\<close>}
You can also refer to the current simpset via an antiquotation. To illustrate
this we implement the function that extracts the theorem names stored in a
@@ -841,8 +841,8 @@
The current simpset can be referred to using @{ML_ind simpset_of in Raw_Simplifier}.
@{ML_matchresult_fake [display,gray]
- "get_thm_names_from_ss @{context}"
- "[\"Nat.of_nat_eq_id\", \"Int.of_int_eq_id\", \"Nat.One_nat_def\", \<dots>]"}
+ \<open>get_thm_names_from_ss @{context}\<close>
+ \<open>["Nat.of_nat_eq_id", "Int.of_int_eq_id", "Nat.One_nat_def", \<dots>]\<close>}
Again, this way of referencing simpsets makes you independent from additions
of lemmas to the simpset by the user, which can potentially cause loops in your
@@ -885,8 +885,8 @@
in more detail in later sections.) An example for this antiquotation is:
@{ML_matchresult_fake [display,gray]
- "@{term_pat \"Suc (?x::nat)\"}"
- "Const (\"Suc\", \"nat \<Rightarrow> nat\") $ Var ((\"x\", 0), \"nat\")"}
+ \<open>@{term_pat "Suc (?x::nat)"}\<close>
+ \<open>Const ("Suc", "nat \<Rightarrow> nat") $ Var (("x", 0), "nat")\<close>}
which shows the internal representation of the term \<open>Suc ?x\<close>. Similarly
we can write an antiquotation for type patterns. Its code is
@@ -981,18 +981,18 @@
The data can be retrieved with the projection functions defined above.
@{ML_matchresult_fake [display, gray]
-"project_int (nth foo_list 0);
-project_bool (nth foo_list 1)"
-"13
-true"}
+\<open>project_int (nth foo_list 0);
+project_bool (nth foo_list 1)\<close>
+\<open>13
+true\<close>}
Notice that we access the integer as an integer and the boolean as
a boolean. If we attempt to access the integer as a boolean, then we get
a runtime error.
@{ML_matchresult_fake [display, gray]
-"project_bool (nth foo_list 0)"
-"*** exception Match raised"}
+\<open>project_bool (nth foo_list 0)\<close>
+\<open>*** exception Match raised\<close>}
This runtime error is the reason why ML is still type-sound despite
containing a universal type.
@@ -1063,8 +1063,8 @@
Section~\ref{sec:theories}). The lookup can now be performed as follows.
@{ML_matchresult_fake [display, gray]
-"lookup @{theory} \"conj\""
-"SOME \"\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q\""}
+\<open>lookup @{theory} "conj"\<close>
+\<open>SOME "\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q"\<close>}
An important point to note is that these tables (and data in general)
need to be treated in a purely functional fashion. Although
@@ -1077,8 +1077,8 @@
and accordingly, @{ML lookup} now produces the introduction rule for @{term "True"}
@{ML_matchresult_fake [display, gray]
-"lookup @{theory} \"conj\""
-"SOME \"True\""}
+\<open>lookup @{theory} "conj"\<close>
+\<open>SOME "True"\<close>}
there are no references involved. This is one of the most fundamental
coding conventions for programming in Isabelle. References
@@ -1096,11 +1096,11 @@
text \<open>
We initialise the reference with the empty list. Consequently a first
- lookup produces @{ML "ref []" in Unsynchronized}.
+ lookup produces @{ML \<open>ref []\<close> in Unsynchronized}.
@{ML_matchresult_fake [display,gray]
- "WrongRefData.get @{theory}"
- "ref []"}
+ \<open>WrongRefData.get @{theory}\<close>
+ \<open>ref []\<close>}
For updating the reference we use the following function
\<close>
@@ -1118,23 +1118,23 @@
text \<open>
A lookup in the current theory gives then the expected list
- @{ML "ref [1]" in Unsynchronized}.
+ @{ML \<open>ref [1]\<close> in Unsynchronized}.
@{ML_matchresult_fake [display,gray]
- "WrongRefData.get @{theory}"
- "ref [1]"}
+ \<open>WrongRefData.get @{theory}\<close>
+ \<open>ref [1]\<close>}
So far everything is as expected. But, the trouble starts if we attempt to
backtrack to the ``point'' before the \isacommand{setup}-command. There, we
would expect that the list is empty again. But since it is stored in a
reference, Isabelle has no control over it. So it is not empty, but still
- @{ML "ref [1]" in Unsynchronized}. Adding to the trouble, if we execute the
- \isacommand{setup}-command again, we do not obtain @{ML "ref [1]" in
+ @{ML \<open>ref [1]\<close> in Unsynchronized}. Adding to the trouble, if we execute the
+ \isacommand{setup}-command again, we do not obtain @{ML \<open>ref [1]\<close> in
Unsynchronized}, but
@{ML_matchresult_fake [display,gray]
- "WrongRefData.get @{theory}"
- "ref [1, 1]"}
+ \<open>WrongRefData.get @{theory}\<close>
+ \<open>ref [1, 1]\<close>}
Now imagine how often you go backwards and forwards in your proof
scripts.\footnote{The same problem can be triggered in the Jedit GUI by
@@ -1180,22 +1180,22 @@
\<open>@{context}\<close> and update it in various ways.
@{ML_matchresult_fake [display,gray]
-"let
+\<open>let
val ctxt0 = @{context}
- val ctxt1 = ctxt0 |> update @{term \"False\"}
- |> update @{term \"True \<and> True\"}
- val ctxt2 = ctxt0 |> update @{term \"1::nat\"}
- val ctxt3 = ctxt2 |> update @{term \"2::nat\"}
+ val ctxt1 = ctxt0 |> update @{term "False"}
+ |> update @{term "True \<and> True"}
+ val ctxt2 = ctxt0 |> update @{term "1::nat"}
+ val ctxt3 = ctxt2 |> update @{term "2::nat"}
in
print ctxt0;
print ctxt1;
print ctxt2;
print ctxt3
-end"
-"Empty!
+end\<close>
+\<open>Empty!
True \<and> True, False
1
-2, 1"}
+2, 1\<close>}
Many functions in Isabelle manage and update data in a similar
fashion. Consequently, such calculations with contexts occur frequently in
@@ -1272,8 +1272,8 @@
@{ML FooRules.get}:
@{ML_matchresult_fake [display,gray]
- "FooRules.get @{context}"
- "[\"True\", \"?C\",\"?B\"]"}
+ \<open>FooRules.get @{context}\<close>
+ \<open>["True", "?C","?B"]\<close>}
Note that this function takes a proof context as argument. This might be
confusing, since the theorem list is stored as theory data. It becomes clear by knowing
@@ -1309,30 +1309,30 @@
function @{ML_ind get in Config} from a proof context
@{ML_matchresult [display,gray]
- "Config.get @{context} bval"
- "true"}
+ \<open>Config.get @{context} bval\<close>
+ \<open>true\<close>}
or directly from a theory using the function @{ML_ind get_global in Config}
@{ML_matchresult [display,gray]
- "Config.get_global @{theory} bval"
- "true"}
+ \<open>Config.get_global @{theory} bval\<close>
+ \<open>true\<close>}
It is also possible to manipulate the configuration values
from the ML-level with the functions @{ML_ind put in Config}
and @{ML_ind put_global in Config}. For example
@{ML_matchresult [display,gray]
- "let
+ \<open>let
val ctxt = @{context}
- val ctxt' = Config.put sval \"foo\" ctxt
- val ctxt'' = Config.put sval \"bar\" ctxt'
+ val ctxt' = Config.put sval "foo" ctxt
+ val ctxt'' = Config.put sval "bar" ctxt'
in
(Config.get ctxt sval,
Config.get ctxt' sval,
Config.get ctxt'' sval)
-end"
- "(\"some string\", \"foo\", \"bar\")"}
+end\<close>
+ \<open>("some string", "foo", "bar")\<close>}
A concrete example for a configuration value is
@{ML_ind simp_trace in Raw_Simplifier}, which switches on trace information