--- a/src/Doc/Prog_Prove/Isar.thy Mon Oct 06 19:55:49 2014 +0200
+++ b/src/Doc/Prog_Prove/Isar.thy Mon Oct 06 21:21:46 2014 +0200
@@ -121,7 +121,7 @@
Labels should be avoided. They interrupt the flow of the reader who has to
scan the context for the point where the label was introduced. Ideally, the
proof is a linear flow, where the output of one step becomes the input of the
-next step, piping the previously proved fact into the next proof, just like
+next step, piping the previously proved fact into the next proof, like
in a UNIX pipe. In such cases the predefined name @{text this} can be used
to refer to the proposition proved in the previous step. This allows us to
eliminate all labels from our proof (we suppress the \isacom{lemma} statement):
@@ -874,7 +874,7 @@
\begin{quote}
\isacom{case} @{text"(evSS m)"}
\end{quote}
-just like \isacom{case}~@{text"(Suc n)"} in earlier structural inductions.
+like \isacom{case}~@{text"(Suc n)"} in earlier structural inductions.
The name @{text m} is an arbitrary choice. As a result,
case @{thm[source] evSS} is derived from a renamed version of
rule @{thm[source] evSS}: @{text"ev m \<Longrightarrow> ev(Suc(Suc m))"}.
@@ -1039,7 +1039,7 @@
\isacom{lemma} @{text[source]"I r s t \<Longrightarrow> \<dots>"}\isanewline
\isacom{proof}@{text"(induction \"r\" \"s\" \"t\" arbitrary: \<dots> rule: I.induct)"}\index{inductionrule@@{text"induction ... rule:"}}\index{arbitrary@@{text"arbitrary:"}}
\end{isabelle}
-Just like for rule inversion, cases that are impossible because of constructor clashes
+Like for rule inversion, cases that are impossible because of constructor clashes
will not show up at all. Here is a concrete example: *}
lemma "ev (Suc m) \<Longrightarrow> \<not> ev m"
--- a/src/Doc/Prog_Prove/Logic.thy Mon Oct 06 19:55:49 2014 +0200
+++ b/src/Doc/Prog_Prove/Logic.thy Mon Oct 06 21:21:46 2014 +0200
@@ -127,7 +127,7 @@
\end{center}
The ASCII forms are \ \texttt{UN x:A.~B} \ and \ \texttt{INT x:A. B} \
where \texttt{x} may occur in \texttt{B}.
-If \texttt{A} is \texttt{UNIV} you can just write \ \texttt{UN x.~B} \ and \ \texttt{INT x. B}.
+If \texttt{A} is \texttt{UNIV} you can write \ \texttt{UN x.~B} \ and \ \texttt{INT x. B}.
Some other frequently useful functions on sets are the following:
\begin{center}
@@ -197,7 +197,7 @@
A proof method that is still incomplete but tries harder than @{text auto} is
\indexed{@{text fastforce}}{fastforce}. It either succeeds or fails, it acts on the first
-subgoal only, and it can be modified just like @{text auto}, e.g.,
+subgoal only, and it can be modified like @{text auto}, e.g.,
with @{text "simp add"}. Here is a typical example of what @{text fastforce}
can do:
*}
@@ -258,7 +258,7 @@
means. For a start, Isabelle does not trust external tools (and in particular
not the translations from Isabelle's logic to those tools!)
and insists on a proof that it can check. This is what \indexed{@{text metis}}{metis} does.
-It is given a list of lemmas and tries to find a proof just using those lemmas
+It is given a list of lemmas and tries to find a proof using just those lemmas
(and pure logic). In contrast to using @{text simp} and friends who know a lot of
lemmas already, using @{text metis} manually is tedious because one has
to find all the relevant lemmas first. But that is precisely what
@@ -352,7 +352,7 @@
@{text "?P"} with @{prop "a=b"} and @{text "?Q"} with @{prop False}.
\end{itemize}
We need not instantiate all unknowns. If we want to skip a particular one we
-can just write @{text"_"} instead, for example @{text "conjI[of _ \"False\"]"}.
+can write @{text"_"} instead, for example @{text "conjI[of _ \"False\"]"}.
Unknowns can also be instantiated by name using \indexed{@{text "where"}}{where}, for example
@{text "conjI[where ?P = \"a=b\""} \isacom{and} @{text"?Q = \"False\"]"}.
--- a/src/Doc/Prog_Prove/Types_and_funs.thy Mon Oct 06 19:55:49 2014 +0200
+++ b/src/Doc/Prog_Prove/Types_and_funs.thy Mon Oct 06 21:21:46 2014 +0200
@@ -46,14 +46,14 @@
Distinctness and injectivity are applied automatically by @{text auto}
and other proof methods. Induction must be applied explicitly.
-Datatype values can be taken apart with case expressions\index{case expression}\index{case expression@@{text "case ... of"}}, for example
+Like in functional programming languages, datatype values can be taken apart
+with case expressions\index{case expression}\index{case expression@@{text "case ... of"}}, for example
\begin{quote}
\noquotes{@{term[source] "(case xs of [] \<Rightarrow> 0 | x # _ \<Rightarrow> Suc x)"}}
\end{quote}
-just like in functional programming languages. Case expressions
-must be enclosed in parentheses.
+Case expressions must be enclosed in parentheses.
-As an example, consider binary trees:
+As an example of a datatype beyond @{typ nat} and @{text list}, consider binary trees:
*}
datatype 'a tree = Tip | Node "'a tree" 'a "'a tree"
@@ -502,7 +502,7 @@
properties will be affected.
The definition of a function @{text f} is a theorem named @{text f_def}
-and can be added to a call of @{text simp} just like any other theorem:
+and can be added to a call of @{text simp} like any other theorem:
\begin{quote}
\isacom{apply}@{text"(simp add: f_def)"}
\end{quote}