# HG changeset patch # User wenzelm # Date 930842654 -7200 # Node ID 27ba88d573993dae79d973413d8f1583a4440866 # Parent 7cb9d3250db7d09f09964c8d0762042394d86716 added prf_asm; diff -r 7cb9d3250db7 -r 27ba88d57399 src/Pure/Isar/outer_syntax.ML --- 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;