author nipkow Mon, 06 Oct 2014 19:37:42 +0200 changeset 58602 ab56811d76c6 parent 58596 877c5ecee253 child 58603 bca419a7f9eb
tuned spaces
 src/Doc/Prog_Prove/Isar.thy file | annotate | diff | comparison | revisions src/Doc/Prog_Prove/Types_and_funs.thy file | annotate | diff | comparison | revisions
--- 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)"}.
--- a/src/Doc/Prog_Prove/Types_and_funs.thy	Mon Oct 06 18:17:44 2014 +0200
+++ b/src/Doc/Prog_Prove/Types_and_funs.thy	Mon Oct 06 19:37:42 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.