--- a/CookBook/FirstSteps.thy Sat Nov 29 21:20:18 2008 +0000
+++ b/CookBook/FirstSteps.thy Sat Dec 13 01:33:22 2008 +0000
@@ -7,9 +7,9 @@
text {*
- Isabelle programming is done in SML. Just like lemmas and proofs, SML-code
+ Isabelle programming is done in ML. Just like lemmas and proofs, ML-code
in Isabelle is part of a theory. If you want to follow the code written in
- this chapter, we assume you are working inside the theory defined by
+ this chapter, we assume you are working inside the theory starting with
\begin{center}
\begin{tabular}{@ {}l}
@@ -49,7 +49,7 @@
\begin{center}
\begin{tabular}{@ {}l}
- \isacommand{theory} CookBook\\
+ \isacommand{theory} FirstSteps\\
\isacommand{imports} Main\\
\isacommand{uses} @{ML_text "\"file_to_be_included.ML\""} @{text "\<dots>"}\\
\isacommand{begin}\\
@@ -82,12 +82,12 @@
The function @{ML "warning"} should only be used for testing purposes, because any
output this function generates will be overwritten as soon as an error is
raised. For printing anything more serious and elaborate, the
- function @{ML tracing} should be used. This function writes all output into
+ function @{ML tracing} is more appropriate. This function writes all output into
a separate tracing buffer. For example
@{ML [display] "tracing \"foo\""}
- It is also possible to redirect the ``channel'' where the @{ML_text "foo"} is
+ It is also possible to redirect the ``channel'' where the string @{ML_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
*}
@@ -152,8 +152,11 @@
In a similar way you can use antiquotations to refer to theorems or simpsets:
- @{ML [display] "@{thm allI}"}
- @{ML [display] "@{simpset}"}
+ @{ML_response_fake [display] "@{thm allI}" "(\<And>x. ?P x) \<Longrightarrow> \<forall>x. ?P x"}
+ @{ML_response_fake [display] "@{simpset}" "\<dots>"}
+
+ (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
avoid explicit bindings for theorems such as
@@ -241,7 +244,7 @@
\begin{readmore}
Types are described in detail in \isccite{sec:types}. Their
- definition and many useful operations can be found in @{ML_file "Pure/type.ML"}.
+ definition and many useful operations can also be found in @{ML_file "Pure/type.ML"}.
\end{readmore}
*}
@@ -350,7 +353,7 @@
We can freely construct and manipulate terms, since they are just
arbitrary unchecked trees. However, we eventually want to see if a
- term is well-formed, or type checks, relative to a theory.
+ term is well-formed, or type-checks, relative to a theory.
Type-checking is done via the function @{ML cterm_of}, which converts
a @{ML_type term} into a @{ML_type cterm}, a \emph{certified} term.
Unlike @{ML_type term}s, which are just trees, @{ML_type
@@ -358,7 +361,7 @@
type-correct, and that can only be constructed via the ``official
interfaces''.
- Type checking is always relative to a theory context. For now we use
+ Type-checking is always relative to a theory context. For now we use
the @{ML "@{theory}"} antiquotation to get hold of the current theory.
For example we can write
@@ -368,7 +371,11 @@
@{ML_response_fake [display] "@{cterm \"(a::nat) + b = c\"}" "a + b = c"}
- A slightly more elaborate example is
+ Attempting
+
+ @{ML_response_fake_both [display] "@{cterm \"1 + True\"}" "Type unification failed \<dots>"}
+
+ yields an error. A slightly more elaborate example is
@{ML_response_fake [display]
"let
@@ -391,8 +398,8 @@
text {*
Just like @{ML_type cterm}s, theorems are abstract objects of type @{ML_type thm}
- that can only be built by going through interfaces, which means that all your proofs
- will be checked.
+ that can only be built by going through interfaces. In effect all proofs
+ are checked.
To see theorems in ``action'', let us give a proof for the following statement
*}
@@ -472,7 +479,8 @@
prop"} is just the identity function and used as a syntactic marker.
\begin{readmore}
- For more on goals see \isccite{sec:tactical-goals}.
+ For more on goals see \isccite{sec:tactical-goals}. (FIXME: in which
+ file is most code for dealing with goals?)
\end{readmore}
Tactics are functions that map a goal state to a (lazy)
@@ -525,7 +533,8 @@
end" "?P \<or> ?Q \<Longrightarrow> ?Q \<or> ?P"}
\begin{readmore}
- To learn more about the function @{ML Goal.prove} see \isccite{sec:results}.
+ To learn more about the function @{ML Goal.prove} see \isccite{sec:results} and
+ the file @{ML_file "Pure/goal.ML"}.
\end{readmore}
--- a/CookBook/Intro.thy Sat Nov 29 21:20:18 2008 +0000
+++ b/CookBook/Intro.thy Sat Dec 13 01:33:22 2008 +0000
@@ -6,9 +6,10 @@
chapter {* Introduction *}
text {*
- The purpose of this cookbook is to guide the reader through the
+ The purpose of this Cookbook is to guide the reader through the
first steps of Isabelle programming, and to provide recipes for
- solving common problems.
+ solving common problems. The code provided in the Cookbook is
+ checked against recent versions of Isabelle.
*}
section {* Intended Audience and Prior Knowledge *}
@@ -16,10 +17,10 @@
text {*
This cookbook targets an audience who already knows how to use Isabelle
for writing theories and proofs. We also assume that readers are
- familiar with Standard ML (SML), the programming language in which
- most of Isabelle is implemented. If you are unfamiliar with either of
+ familiar with the functional programming language ML, the language in
+ which most of Isabelle is implemented. If you are unfamiliar with either of
these two subjects, you should first work through the Isabelle/HOL
- tutorial \cite{isa-tutorial} or Paulson's book on SML
+ tutorial \cite{isa-tutorial} or Paulson's book on ML
\cite{paulson-ml2}.
*}
@@ -57,9 +58,6 @@
learn from other people's code.
\end{description}
- The Cookbook is written in such a way that the code examples in it are
- checked against recent versions of the code.
-
*}
--- a/CookBook/Parsing.thy Sat Nov 29 21:20:18 2008 +0000
+++ b/CookBook/Parsing.thy Sat Dec 13 01:33:22 2008 +0000
@@ -399,7 +399,7 @@
end"
"([\"in\",\"in\",\"in\"],[])"}
- The following function will help us to run examples
+ The following function will help us later to run examples
*}
@@ -427,8 +427,8 @@
\begin{exercise}
A type-identifier, for example @{typ "'a"}, is a token of
- kind @{ML "Keyword" in OuterLex} can be parsed
-
+ kind @{ML "Keyword" in OuterLex}. It can be parsed using
+ the function @{ML OuterParse.type_ident}.
\end{exercise}
--- a/CookBook/Readme.thy Sat Nov 29 21:20:18 2008 +0000
+++ b/CookBook/Readme.thy Sat Dec 13 01:33:22 2008 +0000
@@ -15,7 +15,7 @@
\item You can include references to other Isabelle manuals using the
reference names from those manuals. To do this the following
- four latex commands are defined:
+ four \LaTeX{} commands are defined:
\begin{center}
\begin{tabular}{l|c|c}
@@ -44,7 +44,7 @@
free variables. The latter is used to indicate in which structure or structures the
ML-expression should be evaluated. Examples are:
- \begin{center}
+ \begin{center}\small
\begin{tabular}{l}
@{text "@{ML \"1 + 3\"}"}\\
@{text "@{ML \"a + b\" for a b}"}\\
@@ -67,6 +67,10 @@
the @{ML_text ML_response}-anti\-quotation, except that the
result-specification is not checked. Use this antiquotation
if the result cannot be constructed or the code generates an exception.
+
+ \item[$\bullet$] @{text "@{ML_response_fake_both \"\<dots>\" \"\<dots>\"}"} can be
+ used to show erroneous code. Neither the code nor the response will be
+ chacked.
\item[$\bullet$] @{text "@{ML_file \"\<dots>\"}"} Should be used when
referring to a file. It checks whether the file exists.
--- a/CookBook/antiquote_setup.ML Sat Nov 29 21:20:18 2008 +0000
+++ b/CookBook/antiquote_setup.ML Sat Dec 13 01:33:22 2008 +0000
@@ -43,6 +43,10 @@
let val txt = (space_explode "\n" lhs) @ (add_response_indicator pat)
in ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt txt end)
+fun output_ml_response_fake_both ml src ctxt ((lhs,pat),pos) =
+ let val txt = (space_explode "\n" lhs) @ (add_response_indicator pat)
+ in ThyOutput.output_list (fn _ => fn s => Pretty.str s) src ctxt txt end
+
fun check_file_exists ctxt txt =
if File.exists (Path.append (Path.explode ("~~/src")) (Path.explode txt)) then ()
else error ("Source file " ^ quote txt ^ " does not exist.")
@@ -60,6 +64,8 @@
(output_ml_response ml_pat)),
("ML_response_fake", ThyOutput.args (Scan.lift (OuterParse.position (Args.name -- Args.name)))
(output_ml_response_fake ml_val)),
+ ("ML_response_fake_both", ThyOutput.args (Scan.lift (OuterParse.position (Args.name -- Args.name)))
+ (output_ml_response_fake_both ml_val)),
("ML_struct", ThyOutput.args (Scan.lift (OuterParse.position Args.name)) (output_ml_aux ml_struct)),
("ML_type", ThyOutput.args (Scan.lift (OuterParse.position Args.name)) (output_ml_aux ml_type))];
Binary file cookbook.pdf has changed