isabelle-cookbook: comparison CookBook/FirstSteps.thy

equal deleted inserted replaced

-:fe10da5354a3
+:5dcad9348e4d
 You can print out error messages with the function @{ML error}, as in:
 @{ML_response_fake [display,gray] "if 0=1 then 1 else (error \"foo\")" "\"foo\""}
-See leter on in Section~\ref{sec:printing} for information about printing
+Section~\ref{sec:printing} will give more information about printing
-out data of type @{ML_type term}, @{ML_type cterm} and @{ML_type thm}.
+the main datas tructures of Isabelle, namely @{ML_type term}, @{ML_type cterm}
+and @{ML_type thm}.
 *}
 The code about simpsets extracts the theorem names stored in the
 current simpset.  We get hold of the current simpset with the antiquotation
 @{text "@{simpset}"}.  The function @{ML rep_ss in MetaSimplifier} returns a record
 containing all information about the simpset. The rules of a simpset are
-stored in a \emph{discrimination net} (a datastructure for fast
+stored in a \emph{discrimination net} (a data structure for fast
 indexing). From this net we can extract the entries using the function @{ML
 Net.entries}.
 \begin{readmore}
 \item @{term "{ [x::int] | x. x \<le> -2 }"}
 \end{itemize}
 Hint: The third term is already quite big, and the pretty printer
 may omit parts of it by default. If you want to see all of it, you
-can use the following ML function to set the limit to a value high
+can use the following ML-function to set the limit to a value high
 enough:
 @{ML [display,gray] "print_depth 50"}
 \end{exercise}
 Logic.all x (Logic.mk_implies (P $ x, Q $ x))
 end *}
 text {*
 The reason is that you cannot pass the arguments @{term P}, @{term Q} and
-@{term "tau"} into an antiquotation. For example the following does \emph{not} work:
+@{term "tau"} into an antiquotation. For example the following does \emph{not} work.
 *}
 ML{*fun make_wrong_imp P Q tau = @{prop "\<And>x. P x \<Longrightarrow> Q x"} *}
 text {*
 @{ML_response_fake [display,gray] "@{const_name \"Nil\"}" "List.list.Nil"}
 (FIXME: Is it useful to explain @{text "@{const_syntax}"}?)
-Similarly, you occasionally need to construct types manually. For example
+Although to some extend types of terms can be inferred, there are many
-the function returning a function type is as follows:
+situations where you need to construct types manually, especially
+when defining constants. For example the function returning a function
+type is as follows:
 *}
 ML{*fun make_fun_type tau1 tau2 = Type ("fun",[tau1,tau2]) *}
-text {* This can be equally written as *}
+text {* This can be equally written as: *}
 ML{*fun make_fun_type tau1 tau2 = tau1 --> tau2 *}
 text {*
 assume assm1
 |> forall_elim (cterm_of thy @{term \"t::nat\"});
 val Qt = implies_elim Pt_implies_Qt (assume assm2);
 in
 Qt
 |> implies_intr assm2
 |> implies_intr assm1
 end" "\<lbrakk>\<And>x. P x \<Longrightarrow> Q x; P t\<rbrakk> \<Longrightarrow> Q t"}
 section {* Storing Theorems *}
 section {* Theorem Attributes *}
-section {* Printing Terms, CTerms and Theorems\label{sec:printing} *}
+section {* Printing Terms and Theorems\label{sec:printing} *}
 text {*
-During development, you will occationally feel the need to inspect terms, cterms
+During development, you often want to inspect terms, cterms
-or theorems. Isabelle contains elaborate pretty-printing functions for that, but
+or theorems. Isabelle contains elaborate pretty-printing functions for printing them,
-for quick-and-dirty solutions they are way too unwieldy. A simple way to transform
+but  for quick-and-dirty solutions they are far too unwieldy. A simple way to transform
 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. The string
+This produces a string with some printing directions encoded in it. The string
-can be properly printed, when enclosed in a @{ML warning}.
+can be properly printed by using @{ML warning} foe example.
 @{ML_response_fake [display,gray]
 "warning (Syntax.string_of_term @{context} @{term \"1::nat\"})"
 "\"1\""}
 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 them.
+contains further information about combinators.
 \end{readmore}
-The simplest combinator is @{ML I}, which is just the identity function.
+The simplest combinator is @{ML I}, which is just the identity function defined as
 *}
 ML{*fun I x = x*}
 text {* Another simple combinator is @{ML K}, defined as *}
 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
-returning @{text x}.
+always returning @{text x}.
 The next combinator is reverse application, @{ML "|>"}, defined as:
 *}
 ML{*fun x |> f = f x*}
 |> (fn x => (x, x))
 |> fst
 |> (fn x => x + 4)*}
 text {*
-which increments the argument @{text x} by 5. It does this by first incrementing
+which increments its 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 in

changeset 104	5dcad9348e4d
parent 102	5e309df58557
child 107	258ce361ba1b