# HG changeset patch # User wenzelm # Date 1215689853 -7200 # Node ID fb07f3b328630d37840fd5d7a92fd4b0a3be3e9a # Parent 59b54d80d2ae0746e30f6a7fe76f7296d9c1af4f added is_diag; diff -r 59b54d80d2ae -r fb07f3b32863 src/Pure/Isar/outer_keyword.ML --- a/src/Pure/Isar/outer_keyword.ML Thu Jul 10 13:37:31 2008 +0200 +++ b/src/Pure/Isar/outer_keyword.ML Thu Jul 10 13:37:33 2008 +0200 @@ -49,6 +49,7 @@ val command: string -> T -> unit val is_theory: string -> bool val is_proof: string -> bool + val is_diag: string -> bool end; structure OuterKeyword: OUTER_KEYWORD = @@ -181,4 +182,6 @@ (map kind_of [qed, qed_block, qed_global, prf_heading, prf_goal, prf_block, prf_open, prf_close, prf_chain, prf_decl, prf_asm, prf_asm_goal, prf_script]); +val is_diag = command_category [kind_of diag]; + end;