src/Pure/Pure.thy
changeset 69913 ca515cf61651
parent 69891 def3ec9cdb7e
child 70009 435fb018e8ee
     1.1 --- a/src/Pure/Pure.thy	Thu Mar 14 16:35:58 2019 +0100
     1.2 +++ b/src/Pure/Pure.thy	Thu Mar 14 16:55:06 2019 +0100
     1.3 @@ -15,11 +15,11 @@
     1.4    and "text" "txt" :: document_body
     1.5    and "text_raw" :: document_raw
     1.6    and "default_sort" :: thy_decl
     1.7 -  and "typedecl" "type_synonym" "nonterminal" "judgment"
     1.8 -    "consts" "syntax" "no_syntax" "translations" "no_translations"
     1.9 -    "definition" "abbreviation" "type_notation" "no_type_notation" "notation"
    1.10 -    "no_notation" "axiomatization" "alias" "type_alias" "lemmas" "declare"
    1.11 -    "hide_class" "hide_type" "hide_const" "hide_fact" :: thy_decl
    1.12 +  and "typedecl" "nonterminal" "judgment" "consts" "syntax" "no_syntax" "translations"
    1.13 +    "no_translations" "type_notation" "no_type_notation" "notation" "no_notation" "alias"
    1.14 +    "type_alias" "declare" "hide_class" "hide_type" "hide_const" "hide_fact" :: thy_decl
    1.15 +  and "type_synonym" "definition" "abbreviation" "lemmas" :: thy_defn
    1.16 +  and "axiomatization" :: thy_stmt
    1.17    and "external_file" "bibtex_file" :: thy_load
    1.18    and "generate_file" :: thy_decl
    1.19    and "export_generated_files" :: diag
    1.20 @@ -46,8 +46,8 @@
    1.21    and "instance" :: thy_goal
    1.22    and "overloading" :: thy_decl_block
    1.23    and "code_datatype" :: thy_decl
    1.24 -  and "theorem" "lemma" "corollary" "proposition" :: thy_goal
    1.25 -  and "schematic_goal" :: thy_goal
    1.26 +  and "theorem" "lemma" "corollary" "proposition" :: thy_goal_stmt
    1.27 +  and "schematic_goal" :: thy_goal_stmt
    1.28    and "notepad" :: thy_decl_block
    1.29    and "have" :: prf_goal % "proof"
    1.30    and "hence" :: prf_goal % "proof"