wenzelm@11538: ;;
wenzelm@11538: ;; Keyword classification tables for Isabelle/Isar.
wenzelm@24904: ;; Generated from Pure + Pure-ProofGeneral + HOL + HOLCF + IOA + HOL-Nominal
wenzelm@24904: ;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***
wenzelm@11538: ;;
wenzelm@11538: ;; $Id$
wenzelm@11538: ;;
wenzelm@11538: 
wenzelm@11538: (defconst isar-keywords-major
wenzelm@11538:   '("\\."
wenzelm@15762:     "\\.\\."
wenzelm@11538:     "ML"
wenzelm@11538:     "ML_command"
wenzelm@11538:     "ML_setup"
wenzelm@11538:     "ProofGeneral\\.inform_file_processed"
wenzelm@11538:     "ProofGeneral\\.inform_file_retracted"
wenzelm@11538:     "ProofGeneral\\.kill_proof"
wenzelm@14938:     "ProofGeneral\\.process_pgip"
wenzelm@11538:     "ProofGeneral\\.restart"
wenzelm@11538:     "ProofGeneral\\.undo"
wenzelm@19069:     "abbreviation"
wenzelm@11538:     "also"
wenzelm@11538:     "apply"
wenzelm@11538:     "apply_end"
wenzelm@11538:     "arities"
wenzelm@11538:     "assume"
wenzelm@24904:     "atom_decl"
wenzelm@12040:     "automaton"
skalberg@14223:     "ax_specification"
wenzelm@11538:     "axclass"
wenzelm@18612:     "axiomatization"
wenzelm@11538:     "axioms"
wenzelm@11538:     "back"
wenzelm@11538:     "by"
wenzelm@11538:     "cannot_undo"
wenzelm@11538:     "case"
wenzelm@11538:     "cd"
wenzelm@11538:     "chapter"
haftmann@18552:     "class"
wenzelm@20568:     "class_deps"
wenzelm@11538:     "classes"
wenzelm@11538:     "classrel"
haftmann@20424:     "code_class"
haftmann@20453:     "code_const"
haftmann@22486:     "code_datatype"
wenzelm@22864:     "code_deps"
wenzelm@24866:     "code_exception"
haftmann@20424:     "code_instance"
berghofe@17147:     "code_library"
berghofe@17147:     "code_module"
wenzelm@21203:     "code_modulename"
wenzelm@21203:     "code_moduleprolog"
wenzelm@22084:     "code_monad"
haftmann@24437:     "code_props"
wenzelm@21028:     "code_reserved"
haftmann@22288:     "code_thms"
haftmann@20453:     "code_type"
wenzelm@11538:     "coinductive"
berghofe@23732:     "coinductive_set"
wenzelm@11538:     "commit"
wenzelm@11538:     "constdefs"
wenzelm@11538:     "consts"
wenzelm@11538:     "consts_code"
wenzelm@11538:     "context"
wenzelm@11746:     "corollary"
huffman@16701:     "cpodef"
wenzelm@11538:     "datatype"
wenzelm@22084:     "declaration"
wenzelm@11538:     "declare"
wenzelm@11538:     "def"
wenzelm@11538:     "defaultsort"
wenzelm@11538:     "defer"
wenzelm@11538:     "defer_recdef"
wenzelm@18775:     "definition"
wenzelm@11538:     "defs"
wenzelm@11538:     "disable_pr"
wenzelm@14938:     "display_drafts"
wenzelm@12040:     "domain"
wenzelm@11538:     "done"
wenzelm@11538:     "enable_pr"
wenzelm@11538:     "end"
wenzelm@24904:     "equivariance"
wenzelm@11538:     "exit"
haftmann@24343:     "export_code"
berghofe@13407:     "extract"
berghofe@13407:     "extract_type"
skalberg@14223:     "finalconsts"
wenzelm@11538:     "finally"
wenzelm@17220:     "find_theorems"
wenzelm@11538:     "fix"
wenzelm@16419:     "fixpat"
huffman@16231:     "fixrec"
wenzelm@11538:     "from"
wenzelm@11538:     "full_prf"
krauss@20523:     "fun"
krauss@19564:     "function"
wenzelm@11538:     "global"
wenzelm@17850:     "guess"
wenzelm@11538:     "have"
wenzelm@11538:     "header"
wenzelm@21732:     "help"
wenzelm@11538:     "hence"
wenzelm@11538:     "hide"
wenzelm@11538:     "inductive"
wenzelm@11538:     "inductive_cases"
berghofe@23732:     "inductive_set"
wenzelm@11538:     "init_toplevel"
wenzelm@11538:     "instance"
haftmann@24437:     "instance_proof"
haftmann@24437:     "instantiation"
ballarin@15624:     "interpret"
ballarin@15598:     "interpretation"
wenzelm@19797:     "invoke"
wenzelm@11538:     "judgment"
wenzelm@11538:     "kill"
wenzelm@11538:     "kill_thy"
wenzelm@11538:     "lemma"
wenzelm@11538:     "lemmas"
wenzelm@11538:     "let"
wenzelm@11538:     "local"
wenzelm@12059:     "locale"
wenzelm@11538:     "method_setup"
wenzelm@11538:     "moreover"
wenzelm@11538:     "next"
wenzelm@15703:     "no_syntax"
wenzelm@19255:     "no_translations"
wenzelm@24904:     "nominal_datatype"
wenzelm@24904:     "nominal_inductive"
wenzelm@24904:     "nominal_primrec"
wenzelm@11538:     "nonterminals"
haftmann@19854:     "normal_form"
wenzelm@21203:     "notation"
wenzelm@11538:     "note"
wenzelm@11538:     "obtain"
wenzelm@11538:     "oops"
wenzelm@11538:     "oracle"
wenzelm@11538:     "parse_ast_translation"
wenzelm@11538:     "parse_translation"
huffman@16701:     "pcpodef"
wenzelm@11538:     "pr"
wenzelm@11538:     "prefer"
wenzelm@11538:     "presume"
wenzelm@11538:     "pretty_setmargin"
wenzelm@11538:     "prf"
wenzelm@11538:     "primrec"
wenzelm@21732:     "print_abbrevs"
wenzelm@11538:     "print_antiquotations"
wenzelm@11538:     "print_ast_translation"
wenzelm@24120:     "print_atp_rules"
wenzelm@11538:     "print_attributes"
wenzelm@11538:     "print_binds"
wenzelm@11538:     "print_cases"
wenzelm@11538:     "print_claset"
haftmann@20378:     "print_classes"
haftmann@22288:     "print_codesetup"
wenzelm@11538:     "print_commands"
wenzelm@24120:     "print_configs"
wenzelm@11538:     "print_context"
wenzelm@14938:     "print_drafts"
wenzelm@11538:     "print_facts"
wenzelm@11661:     "print_induct_rules"
ballarin@15598:     "print_interps"
wenzelm@12059:     "print_locale"
wenzelm@12059:     "print_locales"
wenzelm@11538:     "print_methods"
haftmann@24343:     "print_noatp_rules"
ballarin@24642:     "print_orders"
wenzelm@12365:     "print_rules"
wenzelm@11538:     "print_simpset"
wenzelm@19272:     "print_statement"
wenzelm@11538:     "print_syntax"
wenzelm@11538:     "print_theorems"
wenzelm@11538:     "print_theory"
wenzelm@11538:     "print_trans_rules"
wenzelm@11538:     "print_translation"
wenzelm@11538:     "proof"
wenzelm@11538:     "prop"
wenzelm@11538:     "pwd"
wenzelm@11538:     "qed"
berghofe@14109:     "quickcheck"
berghofe@14109:     "quickcheck_params"
wenzelm@11538:     "quit"
berghofe@13407:     "realizability"
berghofe@13407:     "realizers"
wenzelm@11538:     "recdef"
wenzelm@11538:     "recdef_tc"
wenzelm@11538:     "record"
wenzelm@11538:     "redo"
webertj@14349:     "refute"
webertj@14349:     "refute_params"
wenzelm@11538:     "remove_thy"
wenzelm@11538:     "rep_datatype"
wenzelm@11538:     "sect"
wenzelm@11538:     "section"
wenzelm@11538:     "setup"
wenzelm@11538:     "show"
wenzelm@22200:     "simproc_setup"
wenzelm@22864:     "sledgehammer"
wenzelm@11538:     "sorry"
skalberg@14115:     "specification"
wenzelm@11538:     "subsect"
wenzelm@11538:     "subsection"
wenzelm@11538:     "subsubsect"
wenzelm@11538:     "subsubsection"
wenzelm@11538:     "syntax"
wenzelm@11538:     "term"
krauss@19564:     "termination"
wenzelm@11538:     "text"
wenzelm@11538:     "text_raw"
wenzelm@11538:     "then"
wenzelm@11538:     "theorem"
wenzelm@11538:     "theorems"
wenzelm@11538:     "theory"
wenzelm@11538:     "thm"
wenzelm@11538:     "thm_deps"
wenzelm@11538:     "thus"
haftmann@22486:     "thy_deps"
wenzelm@11538:     "token_translation"
wenzelm@11538:     "touch_child_thys"
wenzelm@11538:     "touch_thy"
wenzelm@11538:     "translations"
wenzelm@11538:     "txt"
wenzelm@11538:     "txt_raw"
wenzelm@11538:     "typ"
wenzelm@11538:     "typed_print_translation"
wenzelm@11538:     "typedecl"
wenzelm@11538:     "typedef"
wenzelm@11538:     "types"
wenzelm@11538:     "types_code"
wenzelm@11538:     "ultimately"
wenzelm@11538:     "undo"
wenzelm@11538:     "undos_proof"
wenzelm@18541:     "unfolding"
wenzelm@11538:     "use"
wenzelm@11538:     "use_thy"
wenzelm@12926:     "using"
berghofe@17552:     "value"
wenzelm@11538:     "welcome"
wenzelm@11538:     "with"
wenzelm@11538:     "{"
wenzelm@11538:     "}"))
wenzelm@11538: 
wenzelm@11538: (defconst isar-keywords-minor
wenzelm@12040:   '("actions"
wenzelm@14660:     "advanced"
wenzelm@12040:     "and"
wenzelm@12042:     "assumes"
berghofe@16771:     "attach"
wenzelm@24904:     "avoids"
nipkow@15135:     "begin"
wenzelm@11538:     "binder"
wenzelm@12040:     "compose"
wenzelm@11538:     "concl"
wenzelm@11538:     "congs"
ballarin@16168:     "constrains"
berghofe@17147:     "contains"
wenzelm@12042:     "defines"
wenzelm@11538:     "distinct"
berghofe@17147:     "file"
wenzelm@12042:     "fixes"
wenzelm@19797:     "for"
wenzelm@12040:     "hide_action"
wenzelm@11538:     "hints"
haftmann@22288:     "identifier"
wenzelm@19797:     "if"
nipkow@15141:     "imports"
wenzelm@11538:     "in"
wenzelm@12954:     "includes"
wenzelm@11538:     "induction"
wenzelm@11661:     "infix"
wenzelm@11538:     "infixl"
wenzelm@11538:     "infixr"
wenzelm@12040:     "initially"
wenzelm@11538:     "inject"
wenzelm@12040:     "inputs"
wenzelm@12040:     "internals"
wenzelm@11538:     "is"
wenzelm@12040:     "lazy"
wenzelm@24866:     "local_syntax"
haftmann@24249:     "module_name"
wenzelm@11538:     "monos"
wenzelm@11746:     "morphisms"
wenzelm@12042:     "notes"
wenzelm@18888:     "obtains"
wenzelm@13364:     "open"
krauss@20338:     "otherwise"
wenzelm@11538:     "output"
wenzelm@12040:     "outputs"
wenzelm@11538:     "overloaded"
wenzelm@11618:     "permissive"
wenzelm@12040:     "post"
wenzelm@12040:     "pre"
wenzelm@12040:     "rename"
wenzelm@12040:     "restrict"
krauss@20338:     "sequential"
wenzelm@12935:     "shows"
wenzelm@12040:     "signature"
wenzelm@12040:     "states"
wenzelm@12042:     "structure"
wenzelm@12040:     "to"
wenzelm@12040:     "transitions"
wenzelm@12040:     "transrel"
wenzelm@19633:     "unchecked"
wenzelm@16419:     "uses"
wenzelm@11538:     "where"))
wenzelm@11538: 
wenzelm@11538: (defconst isar-keywords-control
wenzelm@22084:   '("ProofGeneral\\.inform_file_processed"
wenzelm@11538:     "ProofGeneral\\.inform_file_retracted"
wenzelm@11538:     "ProofGeneral\\.kill_proof"
wenzelm@14938:     "ProofGeneral\\.process_pgip"
wenzelm@11538:     "ProofGeneral\\.restart"
wenzelm@11538:     "ProofGeneral\\.undo"
wenzelm@11538:     "cannot_undo"
wenzelm@11538:     "exit"
wenzelm@11538:     "init_toplevel"
wenzelm@11538:     "kill"
wenzelm@11538:     "quit"
wenzelm@11538:     "redo"
wenzelm@11538:     "undo"
wenzelm@11538:     "undos_proof"))
wenzelm@11538: 
wenzelm@11538: (defconst isar-keywords-diag
wenzelm@11538:   '("ML"
wenzelm@11538:     "ML_command"
wenzelm@11538:     "cd"
wenzelm@20568:     "class_deps"
wenzelm@22864:     "code_deps"
haftmann@22288:     "code_thms"
wenzelm@11538:     "commit"
wenzelm@11538:     "disable_pr"
wenzelm@14938:     "display_drafts"
wenzelm@11538:     "enable_pr"
haftmann@24343:     "export_code"
wenzelm@17220:     "find_theorems"
wenzelm@11538:     "full_prf"
wenzelm@11538:     "header"
wenzelm@21732:     "help"
wenzelm@11538:     "kill_thy"
haftmann@20832:     "normal_form"
wenzelm@11538:     "pr"
wenzelm@11538:     "pretty_setmargin"
wenzelm@11538:     "prf"
wenzelm@21732:     "print_abbrevs"
wenzelm@11538:     "print_antiquotations"
wenzelm@24120:     "print_atp_rules"
wenzelm@11538:     "print_attributes"
wenzelm@11538:     "print_binds"
wenzelm@11538:     "print_cases"
wenzelm@11538:     "print_claset"
haftmann@20378:     "print_classes"
haftmann@22288:     "print_codesetup"
wenzelm@11538:     "print_commands"
wenzelm@24120:     "print_configs"
wenzelm@11538:     "print_context"
wenzelm@14938:     "print_drafts"
wenzelm@11538:     "print_facts"
wenzelm@11661:     "print_induct_rules"
ballarin@15598:     "print_interps"
wenzelm@12059:     "print_locale"
wenzelm@12059:     "print_locales"
wenzelm@11538:     "print_methods"
haftmann@24343:     "print_noatp_rules"
ballarin@24642:     "print_orders"
wenzelm@12365:     "print_rules"
wenzelm@11538:     "print_simpset"
wenzelm@19272:     "print_statement"
wenzelm@11538:     "print_syntax"
wenzelm@11538:     "print_theorems"
wenzelm@11538:     "print_theory"
wenzelm@11538:     "print_trans_rules"
wenzelm@11538:     "prop"
wenzelm@11538:     "pwd"
berghofe@14109:     "quickcheck"
webertj@14349:     "refute"
wenzelm@11538:     "remove_thy"
wenzelm@22864:     "sledgehammer"
wenzelm@11538:     "term"
wenzelm@11538:     "thm"
wenzelm@11538:     "thm_deps"
haftmann@22486:     "thy_deps"
wenzelm@11538:     "touch_child_thys"
wenzelm@11538:     "touch_thy"
wenzelm@11538:     "typ"
wenzelm@11538:     "use"
wenzelm@11538:     "use_thy"
berghofe@17552:     "value"
wenzelm@11538:     "welcome"))
wenzelm@11538: 
wenzelm@11538: (defconst isar-keywords-theory-begin
wenzelm@11538:   '("theory"))
wenzelm@11538: 
wenzelm@11538: (defconst isar-keywords-theory-switch
wenzelm@21302:   '())
wenzelm@11538: 
wenzelm@11538: (defconst isar-keywords-theory-end
wenzelm@11538:   '("end"))
wenzelm@11538: 
wenzelm@11538: (defconst isar-keywords-theory-heading
wenzelm@11538:   '("chapter"
wenzelm@11538:     "section"
wenzelm@11538:     "subsection"
wenzelm@11538:     "subsubsection"))
wenzelm@11538: 
wenzelm@11538: (defconst isar-keywords-theory-decl
wenzelm@11538:   '("ML_setup"
wenzelm@19069:     "abbreviation"
wenzelm@11538:     "arities"
wenzelm@24904:     "atom_decl"
wenzelm@12040:     "automaton"
wenzelm@11538:     "axclass"
wenzelm@18612:     "axiomatization"
wenzelm@11538:     "axioms"
haftmann@18552:     "class"
wenzelm@11538:     "classes"
wenzelm@11538:     "classrel"
haftmann@20424:     "code_class"
haftmann@20453:     "code_const"
haftmann@22486:     "code_datatype"
wenzelm@24866:     "code_exception"
haftmann@20424:     "code_instance"
berghofe@17147:     "code_library"
berghofe@17147:     "code_module"
wenzelm@21203:     "code_modulename"
wenzelm@21203:     "code_moduleprolog"
wenzelm@22084:     "code_monad"
haftmann@24437:     "code_props"
wenzelm@21028:     "code_reserved"
haftmann@20453:     "code_type"
wenzelm@11538:     "coinductive"
berghofe@23732:     "coinductive_set"
wenzelm@11538:     "constdefs"
wenzelm@11538:     "consts"
wenzelm@11538:     "consts_code"
wenzelm@21302:     "context"
wenzelm@11538:     "datatype"
wenzelm@22084:     "declaration"
wenzelm@23804:     "declare"
wenzelm@11538:     "defaultsort"
wenzelm@11538:     "defer_recdef"
wenzelm@18775:     "definition"
wenzelm@11538:     "defs"
wenzelm@12040:     "domain"
wenzelm@24904:     "equivariance"
berghofe@13407:     "extract"
berghofe@13407:     "extract_type"
skalberg@14223:     "finalconsts"
wenzelm@16419:     "fixpat"
huffman@16231:     "fixrec"
krauss@20523:     "fun"
wenzelm@11538:     "global"
wenzelm@11538:     "hide"
wenzelm@11538:     "inductive"
berghofe@23732:     "inductive_set"
haftmann@24437:     "instantiation"
wenzelm@11538:     "judgment"
wenzelm@11538:     "lemmas"
wenzelm@11538:     "local"
wenzelm@12059:     "locale"
wenzelm@11538:     "method_setup"
wenzelm@15703:     "no_syntax"
wenzelm@19255:     "no_translations"
wenzelm@24904:     "nominal_datatype"
wenzelm@11538:     "nonterminals"
wenzelm@21203:     "notation"
wenzelm@11538:     "oracle"
wenzelm@11538:     "parse_ast_translation"
wenzelm@11538:     "parse_translation"
wenzelm@11538:     "primrec"
wenzelm@11538:     "print_ast_translation"
wenzelm@11538:     "print_translation"
berghofe@14109:     "quickcheck_params"
berghofe@13407:     "realizability"
berghofe@13407:     "realizers"
wenzelm@11538:     "recdef"
wenzelm@11538:     "record"
webertj@14349:     "refute_params"
wenzelm@11538:     "rep_datatype"
wenzelm@11538:     "setup"
wenzelm@22200:     "simproc_setup"
wenzelm@11538:     "syntax"
wenzelm@11538:     "text"
wenzelm@11538:     "text_raw"
wenzelm@11538:     "theorems"
wenzelm@11538:     "token_translation"
wenzelm@11538:     "translations"
wenzelm@11538:     "typed_print_translation"
wenzelm@11538:     "typedecl"
wenzelm@11538:     "types"
wenzelm@11538:     "types_code"))
wenzelm@11538: 
wenzelm@11538: (defconst isar-keywords-theory-script
wenzelm@23804:   '("inductive_cases"))
wenzelm@11538: 
wenzelm@11538: (defconst isar-keywords-theory-goal
skalberg@14223:   '("ax_specification"
skalberg@14223:     "corollary"
huffman@16701:     "cpodef"
krauss@19564:     "function"
wenzelm@11746:     "instance"
haftmann@24437:     "instance_proof"
ballarin@15598:     "interpretation"
wenzelm@11538:     "lemma"
wenzelm@24904:     "nominal_inductive"
wenzelm@24904:     "nominal_primrec"
huffman@16701:     "pcpodef"
wenzelm@11538:     "recdef_tc"
skalberg@14115:     "specification"
krauss@19564:     "termination"
wenzelm@11538:     "theorem"
wenzelm@11538:     "typedef"))
wenzelm@11538: 
wenzelm@11538: (defconst isar-keywords-qed
wenzelm@11538:   '("\\."
wenzelm@11538:     "\\.\\."
wenzelm@11538:     "by"
wenzelm@11538:     "done"
wenzelm@11538:     "sorry"))
wenzelm@11538: 
wenzelm@11538: (defconst isar-keywords-qed-block
wenzelm@11538:   '("qed"))
wenzelm@11538: 
wenzelm@11538: (defconst isar-keywords-qed-global
wenzelm@11538:   '("oops"))
wenzelm@11538: 
wenzelm@11538: (defconst isar-keywords-proof-heading
wenzelm@11538:   '("sect"
wenzelm@11538:     "subsect"
wenzelm@11538:     "subsubsect"))
wenzelm@11538: 
wenzelm@11538: (defconst isar-keywords-proof-goal
wenzelm@11538:   '("have"
wenzelm@11538:     "hence"
ballarin@15624:     "interpret"
wenzelm@21806:     "invoke"))
wenzelm@11538: 
wenzelm@11538: (defconst isar-keywords-proof-block
wenzelm@11538:   '("next"
wenzelm@11538:     "proof"))
wenzelm@11538: 
wenzelm@11538: (defconst isar-keywords-proof-open
wenzelm@11538:   '("{"))
wenzelm@11538: 
wenzelm@11538: (defconst isar-keywords-proof-close
wenzelm@11538:   '("}"))
wenzelm@11538: 
wenzelm@11538: (defconst isar-keywords-proof-chain
wenzelm@11538:   '("finally"
wenzelm@11538:     "from"
wenzelm@11538:     "then"
wenzelm@11538:     "ultimately"
wenzelm@11538:     "with"))
wenzelm@11538: 
wenzelm@11538: (defconst isar-keywords-proof-decl
wenzelm@11538:   '("also"
wenzelm@11538:     "let"
wenzelm@11538:     "moreover"
wenzelm@11538:     "note"
wenzelm@11538:     "txt"
wenzelm@12926:     "txt_raw"
wenzelm@18541:     "unfolding"
wenzelm@12926:     "using"))
wenzelm@11538: 
wenzelm@11538: (defconst isar-keywords-proof-asm
wenzelm@11538:   '("assume"
wenzelm@11538:     "case"
wenzelm@11538:     "def"
wenzelm@11538:     "fix"
wenzelm@11538:     "presume"))
wenzelm@11538: 
wenzelm@11538: (defconst isar-keywords-proof-asm-goal
wenzelm@17850:   '("guess"
wenzelm@21806:     "obtain"
wenzelm@21806:     "show"
wenzelm@21806:     "thus"))
wenzelm@11538: 
wenzelm@11538: (defconst isar-keywords-proof-script
wenzelm@11538:   '("apply"
wenzelm@11538:     "apply_end"
wenzelm@11538:     "back"
wenzelm@11538:     "defer"
wenzelm@11538:     "prefer"))
wenzelm@11538: 
wenzelm@11538: (provide 'isar-keywords)