--- a/src/Pure/Isar/outer_syntax.ML Thu Jul 01 10:36:38 1999 +0200
+++ b/src/Pure/Isar/outer_syntax.ML Thu Jul 01 17:24:14 1999 +0200
@@ -36,6 +36,7 @@
val prf_block: string
val prf_chain: string
val prf_decl: string
+ val prf_asm: string
val prf_script: string
val kinds: string list
end
@@ -80,10 +81,11 @@
val prf_block = "proof-block";
val prf_chain = "proof-chain";
val prf_decl = "proof-decl";
+ val prf_asm = "proof-asm";
val prf_script = "proof-script";
val kinds = [control, diag, thy_begin, thy_end, thy_heading, thy_decl, thy_goal, qed,
- qed_block, prf_goal, prf_block, prf_chain, prf_decl, prf_script];
+ qed_block, prf_goal, prf_block, prf_chain, prf_decl, prf_asm, prf_script];
end;