--- a/src/Doc/Isar_Ref/Proof.thy Mon Jun 15 10:33:37 2015 +0200
+++ b/src/Doc/Isar_Ref/Proof.thy Mon Jun 15 10:38:09 2015 +0200
@@ -60,12 +60,9 @@
\begin{description}
- \item @{command "notepad"}~@{keyword "begin"} opens a proof state
- without any goal statement. This allows to experiment with Isar,
- without producing any persistent result.
-
- The notepad can be closed by @{command "end"} or discontinued by
- @{command "oops"}.
+ \item @{command "notepad"}~@{keyword "begin"} opens a proof state without
+ any goal statement. This allows to experiment with Isar, without producing
+ any persistent result. The notepad is closed by @{command "end"}.
\end{description}
\<close>