isabelle-cookbook: comparison CookBook/FirstSteps.thy

equal deleted inserted replaced

-:dd8eebae11ec
+:123401a5c8e9
 section {* Theorem Attributes *}
 section {* Printing Terms, CTerms and Theorems\label{sec:printing} *}
 text {*
-It will often be necesseary to inspect terms, cterms or theorems. Isabelle
+You will occationally feel the need to inspect terms, cterms or theorems during
-contains elaborate pretty-printing functions for that, but for quick-and-dirty
+development. Isabelle contains elaborate pretty-printing functions for that, but
-solutions they are too unwieldy. A term can be transformed into a string using
+for quick-and-dirty solutions they are way too unwieldy. A simple way to transform
-the function @{ML Syntax.string_of_term}
+a term into a string is to use the function @{ML Syntax.string_of_term}.
 @{ML_response_fake [display,gray]
 "Syntax.string_of_term @{context} @{term \"1::nat\"}"
 "\"\\^E\\^Fterm\\^E\\^E\\^Fconst\\^Fname=HOL.one_class.one\\^E1\\^E\\^F\\^E\\^E\\^F\\^E\""}
-This produces a string, though with printing directions encoded in it. This
+This produces a string, though with printing directions encoded in it. The string
-can be properly printed, when enclosed in a @{ML warning}
+can be properly printed, when enclosed in a @{ML warning}.
 @{ML_response_fake [display,gray]
 "warning (Syntax.string_of_term @{context} @{term \"1::nat\"})"
 "\"1\""}
-A @{ML_type cterm} can be transformed into a string by the function:
+A @{ML_type cterm} can be transformed into a string by the following function.
 *}
 ML{*fun str_of_cterm ctxt t =
 Syntax.string_of_term ctxt (term_of t)*}
 text {*
-If there are more than one @{ML_type cterm} to be printed, we can use the function
+If there are more than one @{ML_type cterm} to be printed, you can use the function
 @{ML commas} to conveniently separate them.
 *}
 ML{*fun str_of_cterms ctxt ts =
 commas (map (str_of_cterm ctxt) ts)*}
 text {*
-The easiest way to get the string of a theorem, is to transform it
+The easiest way to get the string of a theorem is to transform it
 into a @{ML_type cterm} using the function @{ML crep_thm}.
 *}
 ML{*fun str_of_thm ctxt thm =
 let
 in
 str_of_cterm ctxt prop
 end*}
 text {*
-For more than one theorem, the following function adds commas in between them.
+Again the function @{ML commas} helps with printing more than one theorem.
 *}
 ML{*fun str_of_thms ctxt thms =
 commas (map (str_of_thm ctxt) thms)*}
 actually ease the understanding and also the programming.
 \begin{readmore}
 The most frequently used combinator 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.
+contains further information about them.
 \end{readmore}
 The simplest combinator is @{ML I}, which is just the identity function.
 *}
 ML{*fun K x = fn _ => x*}
 text {*
 @{ML K} ``wraps'' a function around the argument @{text "x"}. However, this
-function ignores its argument. As a result @{ML K} defines a constant function
+function ignores its argument. As a result, @{ML K} defines a constant function
 returning @{text x}.
-The next combinator is reverse application, @{ML "|>"}, defined as
+The next combinator is reverse application, @{ML "|>"}, defined as:
 *}
 ML{*fun x |> f = f x*}
 text {* While just syntactic sugar for the usual function application,
 which increments the argument @{text x} by 5. It does this 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 inside
+lemmas and so on). The reverse application allows you to read what happens in
-the function in a top-down manner. This kind of codeing should also be familiar,
+a top-down manner. This kind of coding should also be familiar,
 if you used Haskell's do-notation. Writing the function @{ML inc_by_five} using
 the reverse application is much clearer than writing
 *}
 ML{*fun inc_by_five x = fst ((fn x => (x, x)) (x + 1)) + 4*}

changeset 101	123401a5c8e9
parent 100	dd8eebae11ec
child 102	5e309df58557