# HG changeset patch
# User wenzelm
# Date 950037238 -3600
# Node ID 4816ba139574bac3a9c399b02774544208538392
# Parent  67d9d52b0b725b1479d045dfd1772e1485aa39f7
added K.qed_global;

diff -r 67d9d52b0b72 -r 4816ba139574 src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Tue Feb 08 20:12:36 2000 +0100
+++ b/src/Pure/Isar/outer_syntax.ML	Tue Feb 08 20:13:58 2000 +0100
@@ -29,6 +29,7 @@
       val thy_goal: string
       val qed: string
       val qed_block: string
+      val qed_global: string
       val prf_goal: string
       val prf_block: string
       val prf_chain: string
@@ -83,6 +84,7 @@
   val thy_goal = "theory-goal";
   val qed = "qed";
   val qed_block = "qed-block";
+  val qed_global = "qed-global";
   val prf_goal = "proof-goal";
   val prf_block = "proof-block";
   val prf_chain = "proof-chain";
@@ -92,7 +94,8 @@
   val prf_script = "proof-script";
 
   val kinds = [control, diag, thy_begin, thy_switch, thy_end, thy_heading, thy_decl, thy_goal,
-    qed, qed_block, prf_goal, prf_block, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script];
+    qed, qed_block, qed_global, prf_goal, prf_block, prf_chain, prf_decl, prf_asm, prf_asm_goal,
+    prf_script];
 end;