# HG changeset patch
# User nipkow
# Date 1412617222 -7200
# Node ID bca419a7f9eb1516f59c460aa9a2fd9c7cd5d18a
# Parent  85fa90262807312d77e9e49933fdeb2c8780b11a# Parent  ab56811d76c656c03ecaff99664ec0226961d76d
merged

diff -r 85fa90262807 -r bca419a7f9eb src/Doc/Prog_Prove/Isar.thy
--- a/src/Doc/Prog_Prove/Isar.thy	Mon Oct 06 19:19:16 2014 +0200
+++ b/src/Doc/Prog_Prove/Isar.thy	Mon Oct 06 19:40:22 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)"}.
diff -r 85fa90262807 -r bca419a7f9eb src/Doc/Prog_Prove/Types_and_funs.thy
--- a/src/Doc/Prog_Prove/Types_and_funs.thy	Mon Oct 06 19:19:16 2014 +0200
+++ b/src/Doc/Prog_Prove/Types_and_funs.thy	Mon Oct 06 19:40:22 2014 +0200
@@ -136,7 +136,7 @@
 Recursive functions are defined with \indexed{\isacom{fun}}{fun} by pattern matching
 over datatype constructors. The order of equations matters, as in
 functional programming languages. However, all HOL functions must be
-total. This simplifies the logic---terms are always defined---but means
+total. This simplifies the logic --- terms are always defined --- but means
 that recursive functions must terminate. Otherwise one could define a
 function @{prop"f n = f n + (1::nat)"} and conclude \mbox{@{prop"(0::nat) = 1"}} by
 subtracting @{term"f n"} on both sides.
@@ -435,7 +435,7 @@
 responsibility not to include simplification rules that can lead to
 nontermination, either on their own or in combination with other
 simplification rules. The right-hand side of a simplification rule should
-always be ``simpler'' than the left-hand side---in some sense. But since
+always be ``simpler'' than the left-hand side --- in some sense. But since
 termination is undecidable, such a check cannot be automated completely
 and Isabelle makes little attempt to detect nontermination.