wenzelm@11538: ;; wenzelm@11538: ;; Keyword classification tables for Isabelle/Isar. wenzelm@33898: ;; Generated from Pure + Pure-ProofGeneral + HOL + HOLCF + IOA + HOL-Boogie + HOL-Nominal + HOL-SMT + HOL-Statespace. wenzelm@24904: ;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT *** wenzelm@11538: ;; wenzelm@11538: wenzelm@11538: (defconst isar-keywords-major wenzelm@11538: '("\\." wenzelm@15762: "\\.\\." wenzelm@25577: "Isabelle\\.command" wenzelm@29607: "Isar\\.begin_document" wenzelm@29607: "Isar\\.define_command" wenzelm@29607: "Isar\\.edit_document" wenzelm@29607: "Isar\\.end_document" wenzelm@11538: "ML" wenzelm@11538: "ML_command" wenzelm@28280: "ML_prf" wenzelm@26394: "ML_val" wenzelm@11538: "ProofGeneral\\.inform_file_processed" wenzelm@11538: "ProofGeneral\\.inform_file_retracted" wenzelm@11538: "ProofGeneral\\.kill_proof" wenzelm@33874: "ProofGeneral\\.pr" 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@28482: "atp_info" wenzelm@28482: "atp_kill" wenzelm@29113: "atp_messages" immler@31039: "atp_minimize" wenzelm@30527: "attribute_setup" wenzelm@12040: "automaton" skalberg@14223: "ax_specification" wenzelm@11538: "axclass" wenzelm@18612: "axiomatization" wenzelm@11538: "axioms" wenzelm@11538: "back" wenzelm@33687: "boogie_end" wenzelm@33687: "boogie_open" wenzelm@33687: "boogie_status" wenzelm@33687: "boogie_vc" 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@27102: "code_abort" haftmann@35223: "code_abstype" haftmann@20424: "code_class" haftmann@20453: "code_const" haftmann@22486: "code_datatype" wenzelm@22864: "code_deps" haftmann@24997: "code_include" haftmann@20424: "code_instance" berghofe@17147: "code_library" berghofe@17147: "code_module" wenzelm@21203: "code_modulename" wenzelm@22084: "code_monad" bulwahn@31106: "code_pred" 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@33840: "domain_isomorphism" 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" kleing@29882: "find_consts" 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: "instantiation" ballarin@15624: "interpret" ballarin@15598: "interpretation" wenzelm@11538: "judgment" wenzelm@11538: "kill" wenzelm@11538: "kill_thy" wenzelm@11538: "lemma" wenzelm@11538: "lemmas" wenzelm@11538: "let" wenzelm@27538: "linear_undo" wenzelm@11538: "local" wenzelm@30463: "local_setup" wenzelm@12059: "locale" wenzelm@11538: "method_setup" wenzelm@11538: "moreover" wenzelm@33840: "new_domain" wenzelm@11538: "next" blanchet@33198: "nitpick" blanchet@33198: "nitpick_params" wenzelm@24945: "no_notation" wenzelm@15703: "no_syntax" wenzelm@19255: "no_translations" wenzelm@24904: "nominal_datatype" wenzelm@24904: "nominal_inductive" berghofe@28656: "nominal_inductive2" 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" haftmann@25516: "overloading" 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@28482: "print_atps" wenzelm@11538: "print_attributes" wenzelm@11538: "print_binds" wenzelm@11538: "print_cases" wenzelm@11538: "print_claset" haftmann@20378: "print_classes" haftmann@31130: "print_codeproc" 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@32804: "print_interps" wenzelm@12059: "print_locale" wenzelm@12059: "print_locales" wenzelm@11538: "print_methods" ballarin@24642: "print_orders" kaliszyk@35279: "print_quotconsts" kaliszyk@35279: "print_quotients" kaliszyk@35279: "print_quotmaps" 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" kaliszyk@35279: "quotient_definition" kaliszyk@35279: "quotient_type" berghofe@13407: "realizability" berghofe@13407: "realizers" wenzelm@11538: "recdef" wenzelm@11538: "recdef_tc" wenzelm@11538: "record" webertj@14349: "refute" webertj@14349: "refute_params" wenzelm@11538: "remove_thy" wenzelm@11538: "rep_datatype" wenzelm@33685: "repdef" wenzelm@11538: "sect" wenzelm@11538: "section" wenzelm@11538: "setup" wenzelm@11538: "show" wenzelm@22200: "simproc_setup" wenzelm@22864: "sledgehammer" wenzelm@33898: "smt_status" wenzelm@11538: "sorry" skalberg@14115: "specification" wenzelm@25176: "statespace" haftmann@24919: "subclass" ballarin@28895: "sublocale" 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: "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" berghofe@26184: "unused_thms" wenzelm@11538: "use" wenzelm@11538: "use_thy" wenzelm@12926: "using" berghofe@17552: "value" haftmann@31130: "values" 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: "congs" ballarin@16168: "constrains" berghofe@17147: "contains" wenzelm@12042: "defines" 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@11661: "infix" wenzelm@11538: "infixl" wenzelm@11538: "infixr" wenzelm@12040: "initially" wenzelm@12040: "inputs" wenzelm@12040: "internals" wenzelm@11538: "is" wenzelm@12040: "lazy" haftmann@24249: "module_name" wenzelm@11538: "monos" wenzelm@11746: "morphisms" wenzelm@12042: "notes" wenzelm@18888: "obtains" wenzelm@13364: "open" wenzelm@11538: "output" wenzelm@12040: "outputs" wenzelm@11538: "overloaded" wenzelm@11618: "permissive" wenzelm@33685: "pervasive" wenzelm@12040: "post" wenzelm@12040: "pre" wenzelm@12040: "rename" wenzelm@12040: "restrict" 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@25577: '("Isabelle\\.command" wenzelm@29607: "Isar\\.begin_document" wenzelm@29607: "Isar\\.define_command" wenzelm@29607: "Isar\\.edit_document" wenzelm@29607: "Isar\\.end_document" wenzelm@25577: "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@27538: "linear_undo" wenzelm@11538: "quit" wenzelm@11538: "undo" wenzelm@11538: "undos_proof")) wenzelm@11538: wenzelm@11538: (defconst isar-keywords-diag wenzelm@26482: '("ML_command" wenzelm@26394: "ML_val" wenzelm@33874: "ProofGeneral\\.pr" wenzelm@28482: "atp_info" wenzelm@28482: "atp_kill" wenzelm@29113: "atp_messages" immler@31039: "atp_minimize" wenzelm@33687: "boogie_status" 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" kleing@29882: "find_consts" wenzelm@17220: "find_theorems" wenzelm@11538: "full_prf" wenzelm@11538: "header" wenzelm@21732: "help" wenzelm@11538: "kill_thy" blanchet@33198: "nitpick" haftmann@20832: "normal_form" wenzelm@11538: "pr" wenzelm@11538: "pretty_setmargin" wenzelm@11538: "prf" wenzelm@21732: "print_abbrevs" wenzelm@11538: "print_antiquotations" wenzelm@28482: "print_atps" wenzelm@11538: "print_attributes" wenzelm@11538: "print_binds" wenzelm@11538: "print_cases" wenzelm@11538: "print_claset" haftmann@20378: "print_classes" haftmann@31130: "print_codeproc" 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@32804: "print_interps" wenzelm@12059: "print_locale" wenzelm@12059: "print_locales" wenzelm@11538: "print_methods" ballarin@24642: "print_orders" kaliszyk@35279: "print_quotconsts" kaliszyk@35279: "print_quotients" kaliszyk@35279: "print_quotmaps" 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@33898: "smt_status" wenzelm@11538: "term" wenzelm@11538: "thm" wenzelm@11538: "thm_deps" haftmann@22486: "thy_deps" wenzelm@11538: "touch_thy" wenzelm@11538: "typ" berghofe@26184: "unused_thms" wenzelm@11538: "use_thy" berghofe@17552: "value" haftmann@31130: "values" 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@26482: '("ML" wenzelm@19069: "abbreviation" wenzelm@11538: "arities" wenzelm@24904: "atom_decl" wenzelm@30527: "attribute_setup" wenzelm@12040: "automaton" wenzelm@11538: "axclass" wenzelm@18612: "axiomatization" wenzelm@11538: "axioms" wenzelm@33687: "boogie_end" wenzelm@33687: "boogie_open" haftmann@18552: "class" wenzelm@11538: "classes" wenzelm@11538: "classrel" haftmann@27102: "code_abort" haftmann@20424: "code_class" haftmann@20453: "code_const" haftmann@22486: "code_datatype" haftmann@24997: "code_include" haftmann@20424: "code_instance" berghofe@17147: "code_library" berghofe@17147: "code_module" wenzelm@21203: "code_modulename" wenzelm@22084: "code_monad" 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@33840: "domain_isomorphism" 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@30463: "local_setup" wenzelm@12059: "locale" wenzelm@11538: "method_setup" wenzelm@33840: "new_domain" blanchet@33198: "nitpick_params" wenzelm@24945: "no_notation" wenzelm@15703: "no_syntax" wenzelm@19255: "no_translations" wenzelm@24904: "nominal_datatype" wenzelm@11538: "nonterminals" wenzelm@21203: "notation" wenzelm@11538: "oracle" haftmann@25516: "overloading" 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" kaliszyk@35279: "quotient_definition" berghofe@13407: "realizability" berghofe@13407: "realizers" wenzelm@11538: "recdef" wenzelm@11538: "record" webertj@14349: "refute_params" wenzelm@33840: "repdef" wenzelm@11538: "setup" wenzelm@22200: "simproc_setup" wenzelm@25176: "statespace" wenzelm@11538: "syntax" wenzelm@11538: "text" wenzelm@11538: "text_raw" wenzelm@11538: "theorems" wenzelm@11538: "translations" wenzelm@11538: "typed_print_translation" wenzelm@11538: "typedecl" wenzelm@11538: "types" wenzelm@26482: "types_code" wenzelm@26482: "use")) 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" wenzelm@33687: "boogie_vc" haftmann@35223: "code_abstype" bulwahn@31106: "code_pred" skalberg@14223: "corollary" huffman@16701: "cpodef" krauss@19564: "function" wenzelm@11746: "instance" ballarin@15598: "interpretation" wenzelm@11538: "lemma" wenzelm@24904: "nominal_inductive" berghofe@28656: "nominal_inductive2" wenzelm@24904: "nominal_primrec" huffman@16701: "pcpodef" kaliszyk@35279: "quotient_type" wenzelm@11538: "recdef_tc" haftmann@27102: "rep_datatype" skalberg@14115: "specification" haftmann@24919: "subclass" ballarin@28895: "sublocale" 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@29607: '("have" wenzelm@11538: "hence" wenzelm@29607: "interpret")) 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@28280: '("ML_prf" wenzelm@28280: "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)