# HG changeset patch
# User nipkow
# Date 1396089699 -3600
# Node ID b61fd250700654152f4d3fc229fa12cb6ed5bdb6
# Parent  42df98d4ab5f628cd67afc2ed7f2e64fe3547564
tuned

diff -r 42df98d4ab5f -r b61fd2507006 src/Doc/ProgProve/Isar.thy
--- a/src/Doc/ProgProve/Isar.thy	Fri Mar 28 21:17:47 2014 +0100
+++ b/src/Doc/ProgProve/Isar.thy	Sat Mar 29 11:41:39 2014 +0100
@@ -203,19 +203,18 @@
   thus "False" by blast
 qed
 
-text{* In the \isacom{have} step the assumption @{prop"surj f"} is now
+text{*
+\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 ask
+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
 referenced by its name @{text s}. The duplication of @{prop"surj f"} in the
 above proofs (once in the statement of the lemma, once in its proof) has been
 eliminated.
 
-\begin{warn}
-Note the dash after the \isacom{proof}
-command.  It is the null method that does nothing to the goal. Leaving it out
-would ask Isabelle to try some suitable introduction rule on the goal @{const
-False}---but there is no suitable introduction rule and \isacom{proof}
-would fail.
-\end{warn}
-
 Stating a lemma with \isacom{assumes}-\isacom{shows} implicitly introduces the
 name \indexed{@{text assms}}{assms} that stands for the list of all assumptions. You can refer
 to individual assumptions by @{text"assms(1)"}, @{text"assms(2)"} etc,