;; ;; Keyword classification tables for Isabelle/Isar. ;; Generated from Pure + Pure-ProofGeneral + FOL + ZF. ;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT *** ;; (defconst isar-keywords-major '("\\." "\\.\\." "Isabelle\\.command" "Isar\\.begin_document" "Isar\\.command" "Isar\\.define_command" "Isar\\.edit_document" "Isar\\.end_document" "Isar\\.insert" "Isar\\.remove" "ML" "ML_command" "ML_prf" "ML_val" "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" "attribute_setup" "axclass" "axiomatization" "axioms" "back" "by" "cannot_undo" "case" "cd" "chapter" "class" "class_deps" "classes" "classrel" "codatatype" "code_datatype" "code_library" "code_module" "coinductive" "commit" "constdefs" "consts" "consts_code" "context" "corollary" "datatype" "declaration" "declare" "def" "defaultsort" "defer" "definition" "defs" "disable_pr" "display_drafts" "done" "enable_pr" "end" "exit" "extract" "extract_type" "finalconsts" "finally" "find_consts" "find_theorems" "fix" "from" "full_prf" "global" "guess" "have" "header" "help" "hence" "hide" "inductive" "inductive_cases" "init_toplevel" "instance" "instantiation" "interpret" "interpretation" "judgment" "kill" "kill_thy" "lemma" "lemmas" "let" "linear_undo" "local" "local_setup" "locale" "method_setup" "moreover" "next" "no_notation" "no_syntax" "no_translations" "nonterminals" "notation" "note" "obtain" "oops" "oracle" "overloading" "parse_ast_translation" "parse_translation" "pr" "prefer" "presume" "pretty_setmargin" "prf" "primrec" "print_abbrevs" "print_antiquotations" "print_ast_translation" "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_locale" "print_locales" "print_methods" "print_rules" "print_simpset" "print_statement" "print_syntax" "print_tcset" "print_theorems" "print_theory" "print_trans_rules" "print_translation" "proof" "prop" "pwd" "qed" "quickcheck" "quickcheck_params" "quit" "realizability" "realizers" "remove_thy" "rep_datatype" "sect" "section" "setup" "show" "simproc_setup" "sorry" "subclass" "sublocale" "subsect" "subsection" "subsubsect" "subsubsection" "syntax" "term" "text" "text_raw" "then" "theorem" "theorems" "theory" "thm" "thm_deps" "thus" "thy_deps" "touch_thy" "translations" "txt" "txt_raw" "typ" "typed_print_translation" "typedecl" "types" "types_code" "ultimately" "undo" "undos_proof" "unfolding" "unused_thms" "use" "use_thy" "using" "welcome" "with" "{" "}")) (defconst isar-keywords-minor '("advanced" "and" "assumes" "attach" "begin" "binder" "case_eqns" "con_defs" "constrains" "contains" "defines" "domains" "elimination" "file" "fixes" "for" "identifier" "if" "imports" "in" "induction" "infix" "infixl" "infixr" "intros" "is" "monos" "notes" "obtains" "open" "output" "overloaded" "recursor_eqns" "shows" "structure" "type_elims" "type_intros" "unchecked" "uses" "where")) (defconst isar-keywords-control '("Isabelle\\.command" "Isar\\.begin_document" "Isar\\.command" "Isar\\.define_command" "Isar\\.edit_document" "Isar\\.end_document" "Isar\\.insert" "Isar\\.remove" "ProofGeneral\\.inform_file_processed" "ProofGeneral\\.inform_file_retracted" "ProofGeneral\\.kill_proof" "ProofGeneral\\.process_pgip" "ProofGeneral\\.restart" "ProofGeneral\\.undo" "cannot_undo" "exit" "init_toplevel" "kill" "linear_undo" "quit" "undo" "undos_proof")) (defconst isar-keywords-diag '("ML_command" "ML_val" "cd" "class_deps" "commit" "disable_pr" "display_drafts" "enable_pr" "find_consts" "find_theorems" "full_prf" "header" "help" "kill_thy" "pr" "pretty_setmargin" "prf" "print_abbrevs" "print_antiquotations" "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_locale" "print_locales" "print_methods" "print_rules" "print_simpset" "print_statement" "print_syntax" "print_tcset" "print_theorems" "print_theory" "print_trans_rules" "prop" "pwd" "quickcheck" "remove_thy" "term" "thm" "thm_deps" "thy_deps" "touch_thy" "typ" "unused_thms" "use_thy" "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" "abbreviation" "arities" "attribute_setup" "axclass" "axiomatization" "axioms" "class" "classes" "classrel" "codatatype" "code_datatype" "code_library" "code_module" "coinductive" "constdefs" "consts" "consts_code" "context" "datatype" "declaration" "declare" "defaultsort" "definition" "defs" "extract" "extract_type" "finalconsts" "global" "hide" "inductive" "instantiation" "judgment" "lemmas" "local" "local_setup" "locale" "method_setup" "no_notation" "no_syntax" "no_translations" "nonterminals" "notation" "oracle" "overloading" "parse_ast_translation" "parse_translation" "primrec" "print_ast_translation" "print_translation" "quickcheck_params" "realizability" "realizers" "rep_datatype" "setup" "simproc_setup" "syntax" "text" "text_raw" "theorems" "translations" "typed_print_translation" "typedecl" "types" "types_code" "use")) (defconst isar-keywords-theory-script '("inductive_cases")) (defconst isar-keywords-theory-goal '("corollary" "instance" "interpretation" "lemma" "subclass" "sublocale" "theorem")) (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")) (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 '("ML_prf" "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)