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\"]"}.