;; ;; Keyword classification tables for Isabelle/Isar. ;; This file was generated from 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)