diff -r 877c5ecee253 -r ab56811d76c6 src/Doc/Prog_Prove/Isar.thy
--- a/src/Doc/Prog_Prove/Isar.thy	Mon Oct 06 18:17:44 2014 +0200
+++ b/src/Doc/Prog_Prove/Isar.thy	Mon Oct 06 19:37:42 2014 +0200
@@ -73,7 +73,7 @@
 Propositions are optionally named formulas. These names can be referred to in
 later \isacom{from} clauses. In the simplest case, a fact is such a name.
 But facts can also be composed with @{text OF} and @{text of} as shown in
-\autoref{sec:forward-proof}---hence the \dots\ in the above grammar.  Note
+\autoref{sec:forward-proof} --- hence the \dots\ in the above grammar.  Note
 that assumptions, intermediate \isacom{have} statements and global lemmas all
 have the same status and are thus collectively referred to as
 \conceptidx{facts}{fact}.
@@ -110,7 +110,7 @@
 \]
 In order to prove @{prop"~ P"}, assume @{text P} and show @{text False}.
 Thus we may assume @{prop"surj f"}. The proof shows that names of propositions
-may be (single!) digits---meaningful names are hard to invent and are often
+may be (single!) digits --- meaningful names are hard to invent and are often
 not necessary. Both \isacom{have} steps are obvious. The second one introduces
 the diagonal set @{term"{x. x \<notin> f x}"}, the key idea in the proof.
 If you wonder why @{text 2} directly implies @{text False}: from @{text 2}
@@ -207,7 +207,7 @@
 \begin{warn}
 Note the hyphen after the \isacom{proof} command.
 It is the null method that does nothing to the goal. Leaving it out would be asking
-Isabelle to try some suitable introduction rule on the goal @{const False}---but
+Isabelle to try some suitable introduction rule on the goal @{const False} --- but
 there is no such rule and \isacom{proof} would fail.
 \end{warn}
 In the \isacom{have} step the assumption @{prop"surj f"} is now
@@ -945,7 +945,7 @@
 \end{warn}
 
 More complicated inductive proofs than the ones we have seen so far
-often need to refer to specific assumptions---just @{text name} or even
+often need to refer to specific assumptions --- just @{text name} or even
 @{text name.prems} and @{text name.IH} can be too unspecific.
 This is where the indexing of fact lists comes in handy, e.g.,
 @{text"name.IH(2)"} or @{text"name.prems(1-2)"}.