;;

;; Keyword classification tables for Isabelle/Isar.

;; This file was generated by Isabelle/HOL/HOL-Nominal -- DO NOT EDIT!

;;

;; $Id$

;;

(defconst isar-keywords-major

  '("\\."

    "\\.\\."

    "ML"

    "ML_command"

    "ML_setup"

    "ProofGeneral\\.inform_file_processed"

    "ProofGeneral\\.inform_file_retracted"

    "ProofGeneral\\.kill_proof"

    "ProofGeneral\\.process_pgip"

    "ProofGeneral\\.restart"

    "ProofGeneral\\.undo"

    "abbreviation"

    "also"

    "apply"

    "apply_end"

    "arities"

    "assume"

    "atom_decl"

    "ax_specification"

    "axclass"

    "axiomatization"

    "axioms"

    "back"

    "by"

    "cannot_undo"

    "case"

    "cd"

    "chapter"

    "class"

    "class_deps"

    "classes"

    "classrel"

    "code_class"

    "code_const"

    "code_datatype"

    "code_deps"

    "code_exception"

    "code_instance"

    "code_library"

    "code_module"

    "code_modulename"

    "code_moduleprolog"

    "code_monad"

    "code_props"

    "code_reserved"

    "code_thms"

    "code_type"

    "coinductive"

    "coinductive_set"

    "commit"

    "constdefs"

    "consts"

    "consts_code"

    "context"

    "corollary"

    "datatype"

    "declaration"

    "declare"

    "def"

    "defaultsort"

    "defer"

    "defer_recdef"

    "definition"

    "defs"

    "disable_pr"

    "display_drafts"

    "done"

    "enable_pr"

    "end"

    "equivariance"

    "exit"

    "export_code"

    "extract"

    "extract_type"

    "finalconsts"

    "finally"

    "find_theorems"

    "fix"

    "from"

    "full_prf"

    "fun"

    "function"

    "global"

    "guess"

    "have"

    "header"

    "help"

    "hence"

    "hide"

    "inductive"

    "inductive_cases"

    "inductive_set"

    "init_toplevel"

    "instance"

    "instance_proof"

    "instantiation"

    "interpret"

    "interpretation"

    "invoke"

    "judgment"

    "kill"

    "kill_thy"

    "lemma"

    "lemmas"

    "let"

    "local"

    "locale"

    "method_setup"

    "moreover"

    "next"

    "no_syntax"

    "no_translations"

    "nominal_datatype"

    "nominal_inductive"

    "nominal_primrec"

    "nonterminals"

    "normal_form"

    "notation"

    "note"

    "obtain"

    "oops"

    "oracle"

    "parse_ast_translation"

    "parse_translation"

    "pr"

    "prefer"

    "presume"

    "pretty_setmargin"

    "prf"

    "primrec"

    "print_abbrevs"

    "print_antiquotations"

    "print_ast_translation"

    "print_atp_rules"

    "print_attributes"

    "print_binds"

    "print_cases"

    "print_claset"

    "print_classes"

    "print_codesetup"

    "print_commands"

    "print_configs"

    "print_context"

    "print_drafts"

    "print_facts"

    "print_induct_rules"

    "print_interps"

    "print_locale"

    "print_locales"

    "print_methods"

    "print_noatp_rules"

    "print_orders"

    "print_rules"

    "print_simpset"

    "print_statement"

    "print_syntax"

    "print_theorems"

    "print_theory"

    "print_trans_rules"

    "print_translation"

    "proof"

    "prop"

    "pwd"

    "qed"

    "quickcheck"

    "quickcheck_params"

    "quit"

    "realizability"

    "realizers"

    "recdef"

    "recdef_tc"

    "record"

    "redo"

    "refute"

    "refute_params"

    "remove_thy"

    "rep_datatype"

    "sect"

    "section"

    "setup"

    "show"

    "simproc_setup"

    "sledgehammer"

    "sorry"

    "specification"

    "subsect"

    "subsection"

    "subsubsect"

    "subsubsection"

    "syntax"

    "term"

    "termination"

    "text"

    "text_raw"

    "then"

    "theorem"

    "theorems"

    "theory"

    "thm"

    "thm_deps"

    "thus"

    "thy_deps"

    "token_translation"

    "touch_child_thys"

    "touch_thy"

    "translations"

    "txt"

    "txt_raw"

    "typ"

    "typed_print_translation"

    "typedecl"

    "typedef"

    "types"

    "types_code"

    "ultimately"

    "undo"

    "undos_proof"

    "unfolding"

    "use"

    "use_thy"

    "using"

    "value"

    "welcome"

    "with"

    "{"

    "}"))

(defconst isar-keywords-minor

  '("advanced"

    "and"

    "assumes"

    "attach"

    "avoids"

    "begin"

    "binder"

    "concl"

    "congs"

    "constrains"

    "contains"

    "defines"

    "distinct"

    "file"

    "fixes"

    "for"

    "freshness_context"

    "hints"

    "identifier"

    "if"

    "imports"

    "in"

    "includes"

    "induction"

    "infix"

    "infixl"

    "infixr"

    "inject"

    "invariant"

    "is"

    "local_syntax"

    "module_name"

    "monos"

    "morphisms"

    "notes"

    "obtains"

    "open"

    "otherwise"

    "output"

    "overloaded"

    "permissive"

    "sequential"

    "shows"

    "structure"

    "unchecked"

    "uses"

    "where"))

(defconst isar-keywords-control

  '("ProofGeneral\\.inform_file_processed"

    "ProofGeneral\\.inform_file_retracted"

    "ProofGeneral\\.kill_proof"

    "ProofGeneral\\.process_pgip"

    "ProofGeneral\\.restart"

    "ProofGeneral\\.undo"

    "cannot_undo"

    "exit"

    "init_toplevel"

    "kill"

    "quit"

    "redo"

    "undo"

    "undos_proof"))

(defconst isar-keywords-diag

  '("ML"

    "ML_command"

    "cd"

    "class_deps"

    "code_deps"

    "code_thms"

    "commit"

    "disable_pr"

    "display_drafts"

    "enable_pr"

    "export_code"

    "find_theorems"

    "full_prf"

    "header"

    "help"

    "kill_thy"

    "normal_form"

    "pr"

    "pretty_setmargin"

    "prf"

    "print_abbrevs"

    "print_antiquotations"

    "print_atp_rules"

    "print_attributes"

    "print_binds"

    "print_cases"

    "print_claset"

    "print_classes"

    "print_codesetup"

    "print_commands"

    "print_configs"

    "print_context"

    "print_drafts"

    "print_facts"

    "print_induct_rules"

    "print_interps"

    "print_locale"

    "print_locales"

    "print_methods"

    "print_noatp_rules"

    "print_orders"

    "print_rules"

    "print_simpset"

    "print_statement"

    "print_syntax"

    "print_theorems"

    "print_theory"

    "print_trans_rules"

    "prop"

    "pwd"

    "quickcheck"

    "refute"

    "remove_thy"

    "sledgehammer"

    "term"

    "thm"

    "thm_deps"

    "thy_deps"

    "touch_child_thys"

    "touch_thy"

    "typ"

    "use"

    "use_thy"

    "value"

    "welcome"))

(defconst isar-keywords-theory-begin

  '("theory"))

(defconst isar-keywords-theory-switch

  '())

(defconst isar-keywords-theory-end

  '("end"))

(defconst isar-keywords-theory-heading

  '("chapter"

    "section"

    "subsection"

    "subsubsection"))

(defconst isar-keywords-theory-decl

  '("ML_setup"

    "abbreviation"

    "arities"

    "atom_decl"

    "axclass"

    "axiomatization"

    "axioms"

    "class"

    "classes"

    "classrel"

    "code_class"

    "code_const"

    "code_datatype"

    "code_exception"

    "code_instance"

    "code_library"

    "code_module"

    "code_modulename"

    "code_moduleprolog"

    "code_monad"

    "code_props"

    "code_reserved"

    "code_type"

    "coinductive"

    "coinductive_set"

    "constdefs"

    "consts"

    "consts_code"

    "context"

    "datatype"

    "declaration"

    "declare"

    "defaultsort"

    "defer_recdef"

    "definition"

    "defs"

    "equivariance"

    "extract"

    "extract_type"

    "finalconsts"

    "fun"

    "global"

    "hide"

    "inductive"

    "inductive_set"

    "instantiation"

    "judgment"

    "lemmas"

    "local"

    "locale"

    "method_setup"

    "no_syntax"

    "no_translations"

    "nominal_datatype"

    "nonterminals"

    "notation"

    "oracle"

    "parse_ast_translation"

    "parse_translation"

    "primrec"

    "print_ast_translation"

    "print_translation"

    "quickcheck_params"

    "realizability"

    "realizers"

    "recdef"

    "record"

    "refute_params"

    "rep_datatype"

    "setup"

    "simproc_setup"

    "syntax"

    "text"

    "text_raw"

    "theorems"

    "token_translation"

    "translations"

    "typed_print_translation"

    "typedecl"

    "types"

    "types_code"))

(defconst isar-keywords-theory-script

  '("inductive_cases"))

(defconst isar-keywords-theory-goal

  '("ax_specification"

    "corollary"

    "function"

    "instance"

    "instance_proof"

    "interpretation"

    "lemma"

    "nominal_inductive"

    "nominal_primrec"

    "recdef_tc"

    "specification"

    "termination"

    "theorem"

    "typedef"))

(defconst isar-keywords-qed

  '("\\."

    "\\.\\."

    "by"

    "done"

    "sorry"))

(defconst isar-keywords-qed-block

  '("qed"))

(defconst isar-keywords-qed-global

  '("oops"))

(defconst isar-keywords-proof-heading

  '("sect"

    "subsect"

    "subsubsect"))

(defconst isar-keywords-proof-goal

  '("have"

    "hence"

    "interpret"

    "invoke"))

(defconst isar-keywords-proof-block

  '("next"

    "proof"))

(defconst isar-keywords-proof-open

  '("{"))

(defconst isar-keywords-proof-close

  '("}"))

(defconst isar-keywords-proof-chain

  '("finally"

    "from"

    "then"

    "ultimately"

    "with"))

(defconst isar-keywords-proof-decl

  '("also"

    "let"

    "moreover"

    "note"

    "txt"

    "txt_raw"

    "unfolding"

    "using"))

(defconst isar-keywords-proof-asm

  '("assume"

    "case"

    "def"

    "fix"

    "presume"))

(defconst isar-keywords-proof-asm-goal

  '("guess"

    "obtain"

    "show"

    "thus"))

(defconst isar-keywords-proof-script

  '("apply"

    "apply_end"

    "back"

    "defer"

    "prefer"))

(provide 'isar-keywords)