qed_block keywords;
authorwenzelm
Wed, 26 May 1999 22:43:27 +0200
changeset 6733 429bbd7ef26d
parent 6732 cf9f66ca9ee3
child 6734 151c07f5b70a
qed_block keywords;
src/Pure/Isar/outer_syntax.ML
--- 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;