src/Pure/Isar/proof.ML

   val invoke_case: string * string option list * attribute list -> state -> state
   val invoke_case_cmd: string * string option list * Attrib.src list -> state -> state
   val begin_block: state -> state
   val next_block: state -> state
   val end_block: state -> state
+  val begin_notepad: Proof.context -> state
+  val end_notepad: state -> Proof.context
   val proof: Method.text option -> state -> state Seq.seq
   val defer: int option -> state -> state Seq.seq
   val prefer: int -> state -> state Seq.seq
   val apply: Method.text -> state -> state Seq.seq
   val apply_end: Method.text -> state -> state Seq.seq

   #> put_facts NONE;
 
 fun end_block state =
   state
   |> assert_forward
+  |> assert_bottom false
   |> close_block
   |> assert_current_goal false
   |> close_block
   |> export_facts state;
+
+
+(* global notepad *)
+
+val begin_notepad =
+  init
+  #> open_block
+  #> map_context (Variable.set_body true)
+  #> open_block;
+
+val end_notepad =
+  assert_forward
+  #> assert_bottom true
+  #> close_block
+  #> assert_current_goal false
+  #> close_block
+  #> context_of;
 
 
 (* sub-proofs *)
 
 fun proof opt_text =