src/Doc/Prog_Prove/Logic.thy

 \begin{center}
 @{thm UNION_eq} \\ @{thm INTER_eq}
 \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}
 \begin{tabular}{l@ {\quad}l}
 @{const_typ set}\index{set@@{const set}} & converts a list to the set of its elements\\

 There is no complete proof method for HOL, not even in theory.
 Hence all our proof methods only differ in how incomplete they are.
 
 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:
 *}
 
 lemma "\<lbrakk> \<forall>xs \<in> A. \<exists>ys. xs = ys @ ys;  us \<in> A \<rbrakk>

 
 text{* We do not explain how the proof was found but what this command
 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
 \isacom{sledgehammer} does for us.
 In this case lemma @{thm[source]append_eq_conv_conj} alone suffices:

 terms syntactically equal by suitable instantiations of unknowns. For example,
 unifying @{text"?P \<and> ?Q"} with \mbox{@{prop"a=b \<and> False"}} instantiates
 @{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\"]"}.
 
 
 \subsection{Rule Application}