'notepad' requires proper nesting of begin/end;
authorwenzelm
Tue Oct 28 13:52:54 2014 +0100 (2014-10-28)
changeset 58801f420225a22d6
parent 58800 bfed1c26caed
child 58802 3cc68ec558b0
'notepad' requires proper nesting of begin/end;
NEWS
src/Doc/Implementation/Isar.thy
src/Doc/Implementation/Proof.thy
src/Doc/ROOT
     1.1 --- a/NEWS	Tue Oct 28 11:42:51 2014 +0100
     1.2 +++ b/NEWS	Tue Oct 28 13:52:54 2014 +0100
     1.3 @@ -14,6 +14,10 @@
     1.4  This supersedes functor Named_Thms, but with a subtle change of
     1.5  semantics due to external visual order vs. internal reverse order.
     1.6  
     1.7 +* Command 'notepad' requires proper nesting of begin/end and its proof
     1.8 +structure in the body: 'oops' is no longer supported here. Minor
     1.9 +INCOMPATIBILITY, use 'sorry' instead.
    1.10 +
    1.11  
    1.12  *** Prover IDE -- Isabelle/Scala/jEdit ***
    1.13  
     2.1 --- a/src/Doc/Implementation/Isar.thy	Tue Oct 28 11:42:51 2014 +0100
     2.2 +++ b/src/Doc/Implementation/Isar.thy	Tue Oct 28 13:52:54 2014 +0100
     2.3 @@ -168,7 +168,8 @@
     2.4      ML_val
     2.5       \<open>val n = Thm.nprems_of (#goal @{Isar.goal});
     2.6        @{assert} (n = 3);\<close>
     2.7 -    oops
     2.8 +    sorry
     2.9 +end
    2.10  
    2.11  text \<open>Here we see 3 individual subgoals in the same way as regular
    2.12    proof methods would do.\<close>
     3.1 --- a/src/Doc/Implementation/Proof.thy	Tue Oct 28 11:42:51 2014 +0100
     3.2 +++ b/src/Doc/Implementation/Proof.thy	Tue Oct 28 13:52:54 2014 +0100
     3.3 @@ -463,7 +463,8 @@
     3.4          Subgoal.focus goal_ctxt 1 goal;
     3.5        val [A, B] = #prems focus;
     3.6        val [(_, x)] = #params focus;\<close>
     3.7 -    oops
     3.8 +    sorry
     3.9 +end
    3.10  
    3.11  text \<open>\medskip The next example demonstrates forward-elimination in
    3.12    a local context, using @{ML Obtain.result}.\<close>
     4.1 --- a/src/Doc/ROOT	Tue Oct 28 11:42:51 2014 +0100
     4.2 +++ b/src/Doc/ROOT	Tue Oct 28 13:52:54 2014 +0100
     4.3 @@ -100,7 +100,7 @@
     4.4      "root.tex"
     4.5  
     4.6  session Implementation (doc) in "Implementation" = "HOL-Proofs" +
     4.7 -  options [document_variants = "implementation"]
     4.8 +  options [document_variants = "implementation", quick_and_dirty]
     4.9    theories
    4.10      Eq
    4.11      Integration