1.1 --- a/etc/isar-keywords-ZF.el	Sat Dec 04 18:41:12 2010 +0100
     1.2 +++ b/etc/isar-keywords-ZF.el	Sat Dec 04 21:26:55 2010 +0100
     1.3 @@ -107,6 +107,7 @@
     1.4      "nonterminals"
     1.5      "notation"
     1.6      "note"
     1.7 +    "notepad"
     1.8      "obtain"
     1.9      "oops"
    1.10      "oracle"
    1.11 @@ -383,6 +384,7 @@
    1.12      "no_type_notation"
    1.13      "nonterminals"
    1.14      "notation"
    1.15 +    "notepad"
    1.16      "oracle"
    1.17      "overloading"
    1.18      "parse_ast_translation"

     2.1 --- a/etc/isar-keywords.el	Sat Dec 04 18:41:12 2010 +0100
     2.2 +++ b/etc/isar-keywords.el	Sat Dec 04 21:26:55 2010 +0100
     2.3 @@ -144,6 +144,7 @@
     2.4      "nonterminals"
     2.5      "notation"
     2.6      "note"
     2.7 +    "notepad"
     2.8      "obtain"
     2.9      "oops"
    2.10      "oracle"
    2.11 @@ -489,6 +490,7 @@
    2.12      "nominal_datatype"
    2.13      "nonterminals"
    2.14      "notation"
    2.15 +    "notepad"
    2.16      "oracle"
    2.17      "overloading"
    2.18      "parse_ast_translation"

     3.1 --- a/src/Pure/Isar/isar_syn.ML	Sat Dec 04 18:41:12 2010 +0100
     3.2 +++ b/src/Pure/Isar/isar_syn.ML	Sat Dec 04 21:26:55 2010 +0100
     3.3 @@ -35,7 +35,8 @@
     3.4  
     3.5  val _ =
     3.6    Outer_Syntax.command "end" "end (local) theory" (Keyword.tag_theory Keyword.thy_end)
     3.7 -    (Scan.succeed (Toplevel.exit o Toplevel.end_local_theory));
     3.8 +    (Scan.succeed
     3.9 +      (Toplevel.exit o Toplevel.end_local_theory o Toplevel.end_proof (K Proof.end_notepad)));
    3.10  
    3.11  
    3.12  
    3.13 @@ -507,6 +508,11 @@
    3.14  val _ = gen_theorem true Thm.corollaryK;
    3.15  
    3.16  val _ =
    3.17 +  Outer_Syntax.local_theory_to_proof "notepad"
    3.18 +    "Isar proof state as formal notepad, without any result" Keyword.thy_decl
    3.19 +    (Parse.begin >> K Proof.begin_notepad);
    3.20 +
    3.21 +val _ =
    3.22    Outer_Syntax.local_theory_to_proof "example_proof"
    3.23      "example proof body, without any result" Keyword.thy_schematic_goal
    3.24      (Scan.succeed

     4.1 --- a/src/Pure/Isar/proof.ML	Sat Dec 04 18:41:12 2010 +0100
     4.2 +++ b/src/Pure/Isar/proof.ML	Sat Dec 04 21:26:55 2010 +0100
     4.3 @@ -76,6 +76,8 @@
     4.4    val begin_block: state -> state
     4.5    val next_block: state -> state
     4.6    val end_block: state -> state
     4.7 +  val begin_notepad: Proof.context -> state
     4.8 +  val end_notepad: state -> Proof.context
     4.9    val proof: Method.text option -> state -> state Seq.seq
    4.10    val defer: int option -> state -> state Seq.seq
    4.11    val prefer: int -> state -> state Seq.seq
    4.12 @@ -767,12 +769,30 @@
    4.13  fun end_block state =
    4.14    state
    4.15    |> assert_forward
    4.16 +  |> assert_bottom false
    4.17    |> close_block
    4.18    |> assert_current_goal false
    4.19    |> close_block
    4.20    |> export_facts state;
    4.21  
    4.22  
    4.23 +(* global notepad *)
    4.24 +
    4.25 +val begin_notepad =
    4.26 +  init
    4.27 +  #> open_block
    4.28 +  #> map_context (Variable.set_body true)
    4.29 +  #> open_block;
    4.30 +
    4.31 +val end_notepad =
    4.32 +  assert_forward
    4.33 +  #> assert_bottom true
    4.34 +  #> close_block
    4.35 +  #> assert_current_goal false
    4.36 +  #> close_block
    4.37 +  #> context_of;
    4.38 +
    4.39 +
    4.40  (* sub-proofs *)
    4.41  
    4.42  fun proof opt_text =

     5.1 --- a/src/Pure/Isar/toplevel.ML	Sat Dec 04 18:41:12 2010 +0100
     5.2 +++ b/src/Pure/Isar/toplevel.ML	Sat Dec 04 21:26:55 2010 +0100
     5.3 @@ -486,12 +486,13 @@
     5.4      let
     5.5        val prf = init int gthy;
     5.6        val skip = ! skip_proofs;
     5.7 -      val schematic = Proof.schematic_goal prf;
     5.8 +      val (is_goal, no_skip) =
     5.9 +        (true, Proof.schematic_goal prf) handle ERROR _ => (false, true);
    5.10      in
    5.11 -      if skip andalso schematic then
    5.12 +      if is_goal andalso skip andalso no_skip then
    5.13          warning "Cannot skip proof of schematic goal statement"
    5.14        else ();
    5.15 -      if skip andalso not schematic then
    5.16 +      if skip andalso not no_skip then
    5.17          SkipProof (0, (finish gthy (Proof.global_skip_proof int prf), gthy))
    5.18        else Proof (Proof_Node.init prf, (finish gthy, gthy))
    5.19      end