--- a/src/Pure/Isar/isar_syn.ML Sat Dec 04 18:41:12 2010 +0100
+++ b/src/Pure/Isar/isar_syn.ML Sat Dec 04 21:26:55 2010 +0100
@@ -35,7 +35,8 @@
val _ =
Outer_Syntax.command "end" "end (local) theory" (Keyword.tag_theory Keyword.thy_end)
- (Scan.succeed (Toplevel.exit o Toplevel.end_local_theory));
+ (Scan.succeed
+ (Toplevel.exit o Toplevel.end_local_theory o Toplevel.end_proof (K Proof.end_notepad)));
@@ -507,6 +508,11 @@
val _ = gen_theorem true Thm.corollaryK;
val _ =
+ Outer_Syntax.local_theory_to_proof "notepad"
+ "Isar proof state as formal notepad, without any result" Keyword.thy_decl
+ (Parse.begin >> K Proof.begin_notepad);
+
+val _ =
Outer_Syntax.local_theory_to_proof "example_proof"
"example proof body, without any result" Keyword.thy_schematic_goal
(Scan.succeed