--- a/src/Pure/Isar/outer_syntax.ML Wed Jun 07 17:14:58 2000 +0200
+++ b/src/Pure/Isar/outer_syntax.ML Thu Jun 08 21:53:44 2000 +0200
@@ -33,6 +33,8 @@
val qed_global: string
val prf_goal: string
val prf_block: string
+ val prf_open: string
+ val prf_close: string
val prf_chain: string
val prf_decl: string
val prf_asm: string
@@ -90,6 +92,8 @@
val qed_global = "qed-global";
val prf_goal = "proof-goal";
val prf_block = "proof-block";
+ val prf_open = "proof-open";
+ val prf_close = "proof-close";
val prf_chain = "proof-chain";
val prf_decl = "proof-decl";
val prf_asm = "proof-asm";
@@ -97,8 +101,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, qed_global, 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_open, prf_close, prf_chain, prf_decl,
+ prf_asm, prf_asm_goal, prf_script];
end;