# HG changeset patch
# User wenzelm
# Date 938803080 -7200
# Node ID 811022c3837eab88ff5f0f68c9554b178a52b303
# Parent  c859160e78b05980add2c28ce296b1e59fd56a8f
added prf_asm_goal;

diff -r c859160e78b0 -r 811022c3837e src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Fri Oct 01 20:37:38 1999 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Fri Oct 01 20:38:00 1999 +0200
@@ -34,6 +34,7 @@
       val prf_chain: string
       val prf_decl: string
       val prf_asm: string
+      val prf_asm_goal: string
       val prf_script: string
       val kinds: string list
     end
@@ -82,10 +83,11 @@
   val prf_chain = "proof-chain";
   val prf_decl = "proof-decl";
   val prf_asm = "proof-asm";
+  val prf_asm_goal = "proof-asm-goal";
   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_script];
+    qed, qed_block, prf_goal, prf_block, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script];
 end;