# HG changeset patch
# User nipkow
# Date 1412623306 -7200
# Node ID 9d5013661ac6f86efd016ada3373caacc7f30372
# Parent  13dfea1621b25bf250d41378089112818c062e5c
tuned

diff -r 13dfea1621b2 -r 9d5013661ac6 src/Doc/Prog_Prove/Isar.thy
--- 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"
diff -r 13dfea1621b2 -r 9d5013661ac6 src/Doc/Prog_Prove/Logic.thy
--- 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\"]"}.
 
diff -r 13dfea1621b2 -r 9d5013661ac6 src/Doc/Prog_Prove/Types_and_funs.thy
--- 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}