# HG changeset patch
# User wenzelm
# Date 1434357489 -7200
# Node ID 932c65dade337f40791a9aeeb61efa8c36ab4899
# Parent  09b04c815fdbd4efbd0409e736a130f04bc8c79b
tuned;

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>