src/Pure/Isar/isar_syn.ML
changeset 40960 9e54eb514a46
parent 40784 177e8cea3e09
child 40965 54b6c9e1c157
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Sat Dec 04 18:41:12 2010 +0100
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Sat Dec 04 21:26:55 2010 +0100
     1.3 @@ -35,7 +35,8 @@
     1.4  
     1.5  val _ =
     1.6    Outer_Syntax.command "end" "end (local) theory" (Keyword.tag_theory Keyword.thy_end)
     1.7 -    (Scan.succeed (Toplevel.exit o Toplevel.end_local_theory));
     1.8 +    (Scan.succeed
     1.9 +      (Toplevel.exit o Toplevel.end_local_theory o Toplevel.end_proof (K Proof.end_notepad)));
    1.10  
    1.11  
    1.12  
    1.13 @@ -507,6 +508,11 @@
    1.14  val _ = gen_theorem true Thm.corollaryK;
    1.15  
    1.16  val _ =
    1.17 +  Outer_Syntax.local_theory_to_proof "notepad"
    1.18 +    "Isar proof state as formal notepad, without any result" Keyword.thy_decl
    1.19 +    (Parse.begin >> K Proof.begin_notepad);
    1.20 +
    1.21 +val _ =
    1.22    Outer_Syntax.local_theory_to_proof "example_proof"
    1.23      "example proof body, without any result" Keyword.thy_schematic_goal
    1.24      (Scan.succeed