--- a/ProgTutorial/FirstSteps.thy Mon Mar 23 09:18:46 2009 +0100
+++ b/ProgTutorial/FirstSteps.thy Mon Mar 23 12:13:21 2009 +0100
@@ -80,7 +80,7 @@
@{ML_response_fake [display,gray] "warning (makestring 1)" "\"1\""}
- However @{ML makestring} only works if the type of what is converted is monomorphic
+ However, @{ML makestring} only works if the type of what is converted is monomorphic
and not a function.
The function @{ML "warning"} should only be used for testing purposes, because any
@@ -92,7 +92,7 @@
@{ML_response_fake [display,gray] "tracing \"foo\"" "\"foo\""}
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 choking on massive
+ printed to a separate file, e.g., to prevent ProofGeneral from choking on massive
amounts of trace output. This redirection can be achieved with the code:
*}
@@ -201,8 +201,8 @@
Theorem @{thm [source] conjI} looks now as follows
@{ML_response_fake [display, gray]
- "warning (str_of_thm_raw @{context} @{thm conjI})"
- "\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q"}
+ "warning (str_of_thm @{context} @{thm conjI})"
+ "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> P \<and> Q"}
Again the function @{ML commas} helps with printing more than one theorem.
*}
@@ -251,7 +251,7 @@
|> (fn x => x + 4)*}
text {*
- which increments its argument @{text x} by 5. It does this by first incrementing
+ which increments its argument @{text x} by 5. It proceeds by first incrementing
the argument by 1 (Line 2); then storing the result in a pair (Line 3); taking
the first component of the pair (Line 4) and finally incrementing the first
component by 4 (Line 5). This kind of cascading manipulations of values is quite
@@ -352,9 +352,9 @@
cannot be merged back into the ``main waterfall''. To do this, you can use
the next combinator.
- The combinator @{ML "`"} is similar to @{ML tap}, but applies a function to the value
- and returns the result together with the value (as a pair). For example
- the function
+ The combinator @{ML "`"} (a backtick) is similar to @{ML tap}, but applies a
+ function to the value and returns the result together with the value (as a
+ pair). For example the function
*}
ML{*fun inc_as_pair x =
@@ -396,7 +396,8 @@
|-> (fn x => fn y => x + y)*}
text {*
- Recall that @{ML "|>"} is the reverse function applications. Recall also that the related
+ 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 "|>>"} and @{ML "||>"} described above have related combinators for function
composition, namely @{ML "#->"}, @{ML "#>>"} and @{ML "##>"}. Using @{ML "#->"},
@@ -412,7 +413,8 @@
(FIXME: find a good exercise for combinators)
\begin{readmore}
- The most frequently used combinator are defined in the files @{ML_file "Pure/library.ML"}
+ The most frequently used combinators are defined in the files @{ML_file
+ "Pure/library.ML"}
and @{ML_file "Pure/General/basics.ML"}. Also \isccite{sec:ML-linear-trans}
contains further information about combinators.
\end{readmore}
@@ -486,20 +488,21 @@
"get_thm_names_from_ss @{simpset}"
"[\"Nat.of_nat_eq_id\", \"Int.of_int_eq_id\", \"Nat.One_nat_def\", \<dots>]"}
- Again, this way or referencing simpsets makes you independent from additions
+ Again, this way of referencing simpsets makes you independent from additions
of lemmas to the simpset by the user that potentially cause loops.
On the ML-level of Isabelle, you often have to work with qualified names;
- these are strings with some additional information, such positional information
+ these are strings with some additional information, such as positional information
and qualifiers. Such bindings can be generated with the antiquotation
- @{text "@{bindin \<dots>}"}.
+ @{text "@{binding \<dots>}"}.
@{ML_response [display,gray]
"@{binding \"name\"}"
"name"}
- An example where a binding is needed is the function @{ML define in LocalTheory}.
- Below this function defines the constant @{term "TrueConj"} as the conjunction
+ An example where a binding is needed is the function @{ML define in
+ LocalTheory}. Below, this function is used to define the constant @{term
+ "TrueConj"} as the conjunction
@{term "True \<and> True"}.
*}
@@ -509,21 +512,21 @@
(Attrib.empty_binding, @{term "True \<and> True"})) *}
text {*
- While antiquotations have many applications, they were originally introduced in order
- to avoid explicit bindings for theorems such as:
+ While antiquotations have many applications, they were originally introduced
+ in order to avoid explicit bindings of theorems such as:
*}
ML{*val allI = thm "allI" *}
text {*
- These bindings are difficult to maintain and also can be accidentally
- overwritten by the user. This often broke Isabelle
+ Such bindings are difficult to maintain and can be overwritten by the
+ user accidentally. This often broke Isabelle
packages. Antiquotations solve this problem, since they are ``linked''
statically at compile-time. However, this static linkage also limits their
usefulness in cases where data needs to be build up dynamically. In the
- course of this chapter you will learn more about these antiquotations:
+ course of this chapter you will learn more about antiquotations:
they can simplify Isabelle programming since one can directly access all
- kinds of logical elements from th ML-level.
+ kinds of logical elements from the ML-level.
*}
section {* Terms and Types *}
@@ -1360,4 +1363,4 @@
ML {*DatatypePackage.get_datatype @{theory} "List.list"*}
-end
\ No newline at end of file
+end