--- a/src/Pure/Isar/outer_syntax.ML Wed May 26 16:51:05 1999 +0200
+++ b/src/Pure/Isar/outer_syntax.ML Wed May 26 22:43:27 1999 +0200
@@ -29,6 +29,7 @@
val thy_decl: string
val thy_goal: string
val qed: string
+ val qed_block: string
val prf_goal: string
val prf_block: string
val prf_chain: string
@@ -70,6 +71,7 @@
val thy_decl = "theory-decl";
val thy_goal = "theory-goal";
val qed = "qed";
+ val qed_block = "qed-block";
val prf_goal = "proof-goal";
val prf_block = "proof-block";
val prf_chain = "proof-chain";
@@ -77,7 +79,7 @@
val prf_script = "proof-script";
val kinds = [control, diag, thy_begin, thy_end, thy_heading, thy_decl, thy_goal, qed,
- prf_goal, prf_block, prf_chain, prf_decl, prf_script];
+ qed_block, prf_goal, prf_block, prf_chain, prf_decl, prf_script];
end;