isabelle-cookbook: comparison ProgTutorial/FirstSteps.thy

equal deleted inserted replaced

-:7305beb69893
+:840b49bfb1cf
 then there is a convenient, though again ``quick-and-dirty'', method for
 converting values into strings, namely the function @{ML makestring}:
 @{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
 output this function generates will be overwritten as soon as an error is
 raised. For printing anything more serious and elaborate, the
 a separate tracing buffer. For example:
 @{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:
 *}
 ML{*val strip_specials =
 let
 text {*
 Theorem @{thm [source] conjI} looks now as follows
 @{ML_response_fake [display, gray]
-"warning (str_of_thm_raw @{context} @{thm conjI})"
+"warning (str_of_thm @{context} @{thm conjI})"
-"\<lbrakk>?P; ?Q\<rbrakk> \<Longrightarrow> ?P \<and> ?Q"}
+"\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> P \<and> Q"}
 Again the function @{ML commas} helps with printing more than one theorem.
 *}
 ML{*fun str_of_thms ctxt thms =
 |> (fn x => (x, x))
 |> fst
 |> (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
 common when dealing with theories (for example by adding a definition, followed by
 lemmas and so on). The reverse application allows you to read what happens in
 intermediate result inside the tracing buffer. The function @{ML tap} can
 only be used for side-calculations, because any value that is computed
 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
+The combinator @{ML "`"} (a backtick) is similar to @{ML tap}, but applies a
-and returns the result together with the value (as a pair). For example
+function to the value and returns the result together with the value (as a
-the function
+pair). For example the function
 *}
 ML{*fun inc_as_pair x =
 x |> `(fn x => x + 1)
 |> (fn (x, y) => (x, y + 1))*}
 ML{*fun double x =
 x |>  (fn x => (x, x))
 |-> (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 "#->"},
 for example, the function @{text double} can also be written as:
 *}
 text {*
 (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}
 *}
 @{ML_response_fake [display,gray]
 "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}.
+An example where a binding is needed is the function @{ML define in
-Below this function defines the constant @{term "TrueConj"} as the conjunction
+LocalTheory}.  Below, this function is used to define the constant @{term
+"TrueConj"} as the conjunction
 @{term "True \<and> True"}.
 *}
 local_setup %gray {*
 snd o LocalTheory.define Thm.internalK
 ((@{binding "TrueConj"}, NoSyn),
 (Attrib.empty_binding, @{term "True \<and> True"})) *}
 text {*
-While antiquotations have many applications, they were originally introduced in order
+While antiquotations have many applications, they were originally introduced
-to avoid explicit bindings for theorems such as:
+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
+Such bindings are difficult to maintain and can be overwritten by the
-overwritten by the user. This often broke Isabelle
+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 *}
 text {*

changeset 196	840b49bfb1cf
parent 192	2fff636e1fa0
child 197	2fe1877f705f