--- a/CookBook/FirstSteps.thy Tue Dec 16 17:37:39 2008 +0100
+++ b/CookBook/FirstSteps.thy Tue Dec 16 17:28:05 2008 +0000
@@ -33,15 +33,16 @@
\isacharverbatimopen\isanewline
\hspace{5mm}@{ML "3 + 4"}\isanewline
\isacharverbatimclose\isanewline
-@{ML_text "> 7"}\smallskip}
+@{text "> 7"}\smallskip}
- Expressions inside \isacommand{ML}-commands are immediately evaluated,
- like ``normal'' Isabelle proof scripts, by using the advance and undo buttons of
+ The @{text [quotes] "> 7"} indicates the response Isabelle prints out when the
+ \isacommand{ML}-command is evaluated. Like ``normal'' Isabelle proof scripts,
+ \isacommand{ML}-commands can be evaluated by using the advance and undo buttons of
your Isabelle environment. The code inside the \isacommand{ML}-command
can also contain value and function bindings, and even those can be
- undone when the proof script is retracted. In what follows we will drop the
- \isacommand{ML} \isa{\isacharverbatimopen \ldots \isacharverbatimclose} whenever
- we show code and its response.
+ undone when the proof script is retracted. For better readability, we will in what
+ follows drop the \isacommand{ML} \isa{\isacharverbatimopen \ldots \isacharverbatimclose}
+ whenever we show code and its response.
Once a portion of code is relatively stable, one usually wants to
export it to a separate ML-file. Such files can then be included in a
@@ -51,7 +52,7 @@
\begin{tabular}{@ {}l}
\isacommand{theory} FirstSteps\\
\isacommand{imports} Main\\
- \isacommand{uses} @{ML_text "\"file_to_be_included.ML\""} @{text "\<dots>"}\\
+ \isacommand{uses} @{text "\"file_to_be_included.ML\""} @{text "\<dots>"}\\
\isacommand{begin}\\
\ldots
\end{tabular}
@@ -67,14 +68,14 @@
in your code. This can be done in a ``quick-and-dirty'' fashion using
the function @{ML "warning"}. For example
- @{ML [display] "warning \"any string\""}
+ @{ML_response_fake [display] "warning \"any string\"" "\"any string\""}
- will print out @{ML_text [quotes] "any string"} inside the response buffer
- of Isabelle. This function expects a string. If you develop under PolyML,
+ will print out @{text [quotes] "any string"} inside the response buffer
+ of Isabelle. 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, for example:
- @{ML [display] "warning (makestring 1)"}
+ @{ML_response_fake [display] "warning (makestring 1)" "1"}
However this only works if the type of what is converted is monomorphic and is not
a function.
@@ -85,9 +86,9 @@
function @{ML tracing} is more appropriate. This function writes all output into
a separate tracing buffer. For example
- @{ML [display] "tracing \"foo\""}
+ @{ML_response_fake [display] "tracing \"foo\"" "\"foo\""}
- It is also possible to redirect the ``channel'' where the string @{ML_text "foo"} is
+ It is also possible to redirect the ``channel'' where the string @{text "foo"} is
printed to a separate file, e.g. to prevent Proof General from choking on massive
amounts of trace output. This redirection can be achieved using the code
*}
@@ -110,7 +111,7 @@
text {*
Calling @{ML "redirect_tracing"} with @{ML "(TextIO.openOut \"foo.bar\")"}
- will cause that all tracing information is printed into the file @{ML_text "foo.bar"}.
+ will cause that all tracing information is printed into the file @{text "foo.bar"}.
*}
@@ -119,17 +120,17 @@
text {*
The main advantage of embedding all code in a theory is that the code can
- contain references to entities defined on the logical level of Isabelle (by
- this we mean definitions, theorems, terms and so on). This is done using
- antiquotations. For example, one can print out the name of the current
+ contain references to entities defined on the logical level of Isabelle. By
+ this we mean definitions, theorems, terms and so on. This kind of reference is
+ realised with antiquotations. For example, one can print out the name of the current
theory by typing
- @{ML_response [display] "Context.theory_name @{theory}" "FirstSteps"}
+ @{ML_response [display] "Context.theory_name @{theory}" "\"FirstSteps\""}
where @{text "@{theory}"} is an antiquotation that is substituted with the
current theory (remember that we assumed we are inside the theory
- @{ML_text FirstSteps}). The name of this theory can be extracted using
+ @{text FirstSteps}). The name of this theory can be extracted with
the function @{ML "Context.theory_name"}.
Note, however, that antiquotations are statically scoped, that is the value is
@@ -142,9 +143,9 @@
text {*
- does \emph{not} return the name of the current theory, if it is run in a
+ does, as its name suggest, \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 @{ML_text "FirstSteps"}, no matter where the
+ that always returns the string @{text [quotes] "FirstSteps"}, no matter where the
function is called. Operationally speaking, the antiquotation @{text "@{theory}"} is
\emph{not} replaced with code that will look up the current theory in
some data structure and return it. Instead, it is literally
@@ -158,7 +159,7 @@
(FIXME: what does a simpset look like? It seems to be the same problem
like tokens.)
- While antiquotations have many applications, they were originally introduced to
+ While antiquotations nowadays have many applications, they were originally introduced to
avoid explicit bindings for theorems such as
*}
@@ -167,11 +168,11 @@
*}
text {*
- These bindings were difficult to maintain and also could be accidentally
- overwritten by the user. This usually broke definitional
+ These bindings were difficult to maintain and also could accidentally
+ be overwritten by the user. This usually broke definitional
packages. Antiquotations solve this problem, since they are ``linked''
statically at compile-time. However, that also sometimes limits their
- applicability. In the course of this introduction, we will learn more about
+ usefulness. In the course of this introduction, we will learn more about
these antiquotations: they greatly simplify Isabelle programming since one
can directly access all kinds of logical elements from ML.
@@ -289,10 +290,10 @@
@{text "+"} are more complex than one first expects, namely
\begin{center}
- @{ML_text "HOL.zero_class.zero"} and @{ML_text "HOL.plus_class.plus"}.
+ @{text "HOL.zero_class.zero"} and @{text "HOL.plus_class.plus"}.
\end{center}
- The extra prefixes @{ML_text zero_class} and @{ML_text plus_class} are present because
+ The extra prefixes @{text zero_class} and @{text plus_class} are present because
these constants are defined within type classes; the prefix @{text "HOL"} indicates in
which theory they are defined. Guessing such internal names can sometimes be quite hard.
Therefore Isabelle provides the antiquotation @{text "@{const_name \<dots>}"} which does the
@@ -332,7 +333,7 @@
text {*
\begin{exercise}\label{fun:revsum}
- Write a function @{ML_text "rev_sum : term -> term"} that takes a
+ Write a function @{text "rev_sum : term -> term"} that takes a
term of the form @{text "t\<^isub>1 + t\<^isub>2 + \<dots> + t\<^isub>n"} (whereby @{text "i"} might be zero)
and returns the reversed sum @{text "t\<^isub>n + \<dots> + t\<^isub>2 + t\<^isub>1"}. Assume
the @{text "t\<^isub>i"} can be arbitrary expressions and also note that @{text "+"}