--- a/src/Pure/Isar/keyword.ML Mon Sep 02 11:03:02 2013 +0200
+++ b/src/Pure/Isar/keyword.ML Mon Sep 02 16:10:26 2013 +0200
@@ -36,6 +36,7 @@
val prf_decl: T
val prf_asm: T
val prf_asm_goal: T
+ val prf_asm_goal_script: T
val prf_script: T
val kinds: T list
val tag: string -> T -> T
@@ -115,13 +116,14 @@
val prf_decl = kind "prf_decl";
val prf_asm = kind "prf_asm";
val prf_asm_goal = kind "prf_asm_goal";
+val prf_asm_goal_script = kind "prf_asm_goal_script";
val prf_script = kind "prf_script";
val kinds =
[control, diag, thy_begin, thy_end, thy_heading1, thy_heading2, thy_heading3, thy_heading4,
thy_load, thy_decl, thy_script, thy_goal, qed, qed_block, qed_global,
prf_heading2, prf_heading3, prf_heading4, prf_goal, prf_block, prf_open,
- prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script];
+ prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_asm_goal_script, prf_script];
(* tags *)
@@ -242,14 +244,14 @@
val is_proof = command_category
[qed, qed_block, qed_global, prf_heading2, prf_heading3, prf_heading4,
prf_goal, prf_block, prf_open, prf_close, prf_chain, prf_decl,
- prf_asm, prf_asm_goal, prf_script];
+ prf_asm, prf_asm_goal, prf_asm_goal_script, prf_script];
val is_proof_body = command_category
- [diag, prf_heading2, prf_heading3, prf_heading4, prf_block, prf_open,
- prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script];
+ [diag, prf_heading2, prf_heading3, prf_heading4, prf_block, prf_open, prf_close, prf_chain,
+ prf_decl, prf_asm, prf_asm_goal, prf_asm_goal_script, prf_script];
val is_theory_goal = command_category [thy_goal];
-val is_proof_goal = command_category [prf_goal, prf_asm_goal];
+val is_proof_goal = command_category [prf_goal, prf_asm_goal, prf_asm_goal_script];
val is_qed = command_category [qed, qed_block];
val is_qed_global = command_category [qed_global];