--- 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 ***
--- 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>
--- 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>
--- 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