diff -r 09b04c815fdb -r 932c65dade33 src/Doc/Isar_Ref/Proof.thy
--- 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>