# HG changeset patch
# User wenzelm
# Date 1414500774 -3600
# Node ID f420225a22d6fb4956220efff16e0cd340cd9aef
# Parent  bfed1c26caed55596ff0fe5f6e51534d64418967
'notepad' requires proper nesting of begin/end;

diff -r bfed1c26caed -r f420225a22d6 NEWS
--- a/NEWS	Tue Oct 28 11:42:51 2014 +0100
+++ b/NEWS	Tue Oct 28 13:52:54 2014 +0100
@@ -14,6 +14,10 @@
 This supersedes functor Named_Thms, but with a subtle change of
 semantics due to external visual order vs. internal reverse order.
 
+* Command 'notepad' requires proper nesting of begin/end and its proof
+structure in the body: 'oops' is no longer supported here. Minor
+INCOMPATIBILITY, use 'sorry' instead.
+
 
 *** Prover IDE -- Isabelle/Scala/jEdit ***
 
diff -r bfed1c26caed -r f420225a22d6 src/Doc/Implementation/Isar.thy
--- a/src/Doc/Implementation/Isar.thy	Tue Oct 28 11:42:51 2014 +0100
+++ b/src/Doc/Implementation/Isar.thy	Tue Oct 28 13:52:54 2014 +0100
@@ -168,7 +168,8 @@
     ML_val
      \<open>val n = Thm.nprems_of (#goal @{Isar.goal});
       @{assert} (n = 3);\<close>
-    oops
+    sorry
+end
 
 text \<open>Here we see 3 individual subgoals in the same way as regular
   proof methods would do.\<close>
diff -r bfed1c26caed -r f420225a22d6 src/Doc/Implementation/Proof.thy
--- a/src/Doc/Implementation/Proof.thy	Tue Oct 28 11:42:51 2014 +0100
+++ b/src/Doc/Implementation/Proof.thy	Tue Oct 28 13:52:54 2014 +0100
@@ -463,7 +463,8 @@
         Subgoal.focus goal_ctxt 1 goal;
       val [A, B] = #prems focus;
       val [(_, x)] = #params focus;\<close>
-    oops
+    sorry
+end
 
 text \<open>\medskip The next example demonstrates forward-elimination in
   a local context, using @{ML Obtain.result}.\<close>
diff -r bfed1c26caed -r f420225a22d6 src/Doc/ROOT
--- a/src/Doc/ROOT	Tue Oct 28 11:42:51 2014 +0100
+++ b/src/Doc/ROOT	Tue Oct 28 13:52:54 2014 +0100
@@ -100,7 +100,7 @@
     "root.tex"
 
 session Implementation (doc) in "Implementation" = "HOL-Proofs" +
-  options [document_variants = "implementation"]
+  options [document_variants = "implementation", quick_and_dirty]
   theories
     Eq
     Integration