--- a/ProgTutorial/FirstSteps.thy Tue Nov 03 13:57:03 2009 +0100
+++ b/ProgTutorial/FirstSteps.thy Thu Nov 05 10:30:59 2009 +0100
@@ -89,7 +89,7 @@
\end{quote}
However, both commands will only play minor roles in this tutorial (we will
- always arrange that the ML-code is defined outside of proofs).
+ always arrange that the ML-code is defined outside proofs).
Once a portion of code is relatively stable, you usually want to export it
to a separate ML-file. Such files can then be included somewhere inside a
@@ -130,7 +130,7 @@
section {* Printing and Debugging\label{sec:printing} *}
text {*
- During development you might find it necessary to inspect some data in your
+ 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
@@ -156,7 +156,7 @@
@{ML_response_eq [display,gray] "tracing \"foo\"" "\"foo\"" with "(op =)"}
It is also possible to redirect the ``channel'' where the string @{text
- "foo"} is printed to a separate file, e.g., to prevent ProofGeneral from
+ "foo"} is printed to a separate file, e.g., in order to prevent ProofGeneral from
choking on massive amounts of trace output. This redirection can be achieved
with the code:
*}
@@ -219,7 +219,7 @@
thm}. Isabelle contains elaborate pretty-printing functions for printing
them (see Section \ref{sec:pretty}), but for quick-and-dirty solutions they
are a bit unwieldy. One way to transform a term into a string is to use the
- function @{ML_ind string_of_term in Syntax} in the structure @{ML_struct
+ function @{ML_ind string_of_term in Syntax} from the structure @{ML_struct
Syntax}. For more convenience, we bind this function to the toplevel.
*}
@@ -254,8 +254,8 @@
commas (map (string_of_term ctxt) ts)*}
text {*
- You can also print out term together with type information.
- This can be achieved by setting the reference @{ML_ind show_types in Syntax}
+ You can also print out terms together with typing information.
+ For this you need to set the reference @{ML_ind show_types in Syntax}
to @{ML true}.
*}
@@ -270,7 +270,8 @@
where @{text 1} and @{text x} are displayed with their inferred type.
Even more type information can be printed by setting
- @{ML_ind show_all_types in Syntax} to @{ML true}. We obtain then
+ the reference @{ML_ind show_all_types in Syntax} to @{ML true}.
+ We obtain then
*}
(*<*)ML %linenos {*show_all_types := true*}
(*>*)
@@ -279,6 +280,7 @@
"tracing (string_of_term @{context} @{term \"(1::nat, x)\"})"
"(Pair::nat \<Rightarrow> 'a \<Rightarrow> nat \<times> 'a) (1::nat) (x::'a)"}
+ where @{term Pair} is the term-constructor for products.
Other references that influence printing are @{ML_ind show_brackets in Syntax}
and @{ML_ind show_sorts in Syntax}.
*}
@@ -336,7 +338,7 @@
string_of_term ctxt (prop_of (no_vars ctxt thm))*}
text {*
- Theorem @{thm [source] conjI} is now printed as follows:
+ With this function, theorem @{thm [source] conjI} is now printed as follows:
@{ML_response_fake [display, gray]
"tracing (string_of_thm_no_vars @{context} @{thm conjI})"
@@ -359,7 +361,7 @@
@{ML_file "Pure/Syntax/printer.ML"}.
\end{readmore}
- Note that when printing out several ``parcels'' of information that
+ Note that for printing out several ``parcels'' of information that
semantically belong together, like a warning message consisting of
a term and its type, you should try to keep this information together in a
single string. Therefore do \emph{not} print out information as
@@ -378,15 +380,16 @@
and second half."}
To ease this kind of string manipulations, there are a number
- of library functions. For example, the function @{ML_ind cat_lines in Library}
- concatenates a list of strings and inserts newlines.
+ 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_response [display, gray]
"cat_lines [\"foo\", \"bar\"]"
"\"foo\\nbar\""}
- Section \ref{sec:pretty} will also explain the infrastructure of Isabelle
- that helps with more elaborate pretty printing.
+ Section \ref{sec:pretty} will also explain the infrastructure that Isabelle
+ provides for more elaborate pretty printing.
\begin{readmore}
Most of the basic string functions of Isabelle are defined in
@@ -508,6 +511,7 @@
function @{ML_ind list_comb in Term} to the 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.
+
Functions like @{ML apply_fresh_args} are often needed when constructing
terms with fresh variables. The
infrastructure helps tremendously to avoid any name clashes. Consider for
@@ -531,9 +535,9 @@
*}
ML{*val inc_by_six =
- (fn x => x + 1)
- #> (fn x => x + 2)
- #> (fn x => x + 3)*}
+ (fn x => x + 1) #>
+ (fn x => x + 2) #>
+ (fn x => x + 3)*}
text {*
which is the function composed of first the increment-by-one function and then
--- a/ProgTutorial/General.thy Tue Nov 03 13:57:03 2009 +0100
+++ b/ProgTutorial/General.thy Thu Nov 05 10:30:59 2009 +0100
@@ -362,9 +362,9 @@
@{ML_response_fake [display,gray]
"let
- val app = Bound 0 $ Free (\"x\", @{typ nat})
+ val body = Bound 0 $ Free (\"x\", @{typ nat})
in
- Term.dest_abs (\"x\", @{typ \"nat \<Rightarrow> bool\"}, app)
+ Term.dest_abs (\"x\", @{typ \"nat \<Rightarrow> bool\"}, body)
end"
"(\"xa\", Free (\"xa\", \"nat \<Rightarrow> bool\") $ Free (\"x\", \"nat\"))"}
@@ -387,7 +387,7 @@
text {*
\begin{readmore}
There are many functions in @{ML_file "Pure/term.ML"}, @{ML_file
- "Pure/logic.ML"} and @{ML_file "HOL/Tools/hologic.ML"} that make such manual
+ "Pure/logic.ML"} and @{ML_file "HOL/Tools/hologic.ML"} that make manual
constructions of terms and types easier.
\end{readmore}
--- a/ProgTutorial/Parsing.thy Tue Nov 03 13:57:03 2009 +0100
+++ b/ProgTutorial/Parsing.thy Thu Nov 05 10:30:59 2009 +0100
@@ -694,7 +694,8 @@
FIXME:
@{ML_ind parse_term in Syntax} @{ML_ind check_term in Syntax}
@{ML_ind parse_typ in Syntax} @{ML_ind check_typ in Syntax}
-
+ @{ML_ind read_term in Syntax} @{ML_ind read_term in Syntax}
+
*}
Binary file progtutorial.pdf has changed