wenzelm@12176: ;;
wenzelm@52442: ;; Keyword classification tables for Isabelle/Isar.
wenzelm@52442: ;; Generated from Pure + ZF.
wenzelm@24904: ;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***
wenzelm@12176: ;;
wenzelm@12176: 
wenzelm@12176: (defconst isar-keywords-major
wenzelm@12176:   '("\\."
wenzelm@12176:     "\\.\\."
wenzelm@25577:     "Isabelle\\.command"
wenzelm@12176:     "ML"
wenzelm@12176:     "ML_command"
wenzelm@48867:     "ML_file"
wenzelm@28261:     "ML_prf"
wenzelm@26394:     "ML_val"
wenzelm@12176:     "ProofGeneral\\.inform_file_processed"
wenzelm@12176:     "ProofGeneral\\.inform_file_retracted"
wenzelm@12176:     "ProofGeneral\\.kill_proof"
wenzelm@33874:     "ProofGeneral\\.pr"
wenzelm@14937:     "ProofGeneral\\.process_pgip"
wenzelm@12176:     "ProofGeneral\\.restart"
wenzelm@12176:     "ProofGeneral\\.undo"
wenzelm@19069:     "abbreviation"
wenzelm@12176:     "also"
wenzelm@12176:     "apply"
wenzelm@12176:     "apply_end"
wenzelm@12176:     "assume"
wenzelm@30527:     "attribute_setup"
haftmann@18702:     "axiomatization"
wenzelm@12176:     "back"
wenzelm@47057:     "bundle"
wenzelm@12176:     "by"
wenzelm@12176:     "cannot_undo"
wenzelm@12176:     "case"
wenzelm@12176:     "cd"
wenzelm@12176:     "chapter"
haftmann@18552:     "class"
wenzelm@20568:     "class_deps"
bulwahn@31107:     "codatatype"
haftmann@22486:     "code_datatype"
bulwahn@31107:     "coinductive"
wenzelm@12176:     "commit"
wenzelm@12176:     "consts"
wenzelm@12176:     "context"
wenzelm@12176:     "corollary"
bulwahn@31107:     "datatype"
wenzelm@22084:     "declaration"
wenzelm@12176:     "declare"
wenzelm@12176:     "def"
wenzelm@36455:     "default_sort"
wenzelm@12176:     "defer"
wenzelm@18775:     "definition"
wenzelm@12176:     "defs"
wenzelm@12176:     "disable_pr"
wenzelm@14937:     "display_drafts"
wenzelm@12176:     "done"
wenzelm@12176:     "enable_pr"
wenzelm@12176:     "end"
wenzelm@12176:     "exit"
berghofe@13407:     "extract"
berghofe@13407:     "extract_type"
wenzelm@12176:     "finally"
kleing@29882:     "find_consts"
wenzelm@17220:     "find_theorems"
wenzelm@12176:     "fix"
wenzelm@12176:     "from"
wenzelm@12176:     "full_prf"
wenzelm@17850:     "guess"
wenzelm@12176:     "have"
wenzelm@12176:     "header"
wenzelm@21732:     "help"
wenzelm@12176:     "hence"
wenzelm@36180:     "hide_class"
wenzelm@36180:     "hide_const"
wenzelm@36180:     "hide_fact"
wenzelm@36180:     "hide_type"
wenzelm@47057:     "include"
wenzelm@47057:     "including"
bulwahn@31107:     "inductive"
bulwahn@31107:     "inductive_cases"
wenzelm@12176:     "init_toplevel"
wenzelm@12176:     "instance"
wenzelm@24866:     "instantiation"
ballarin@15624:     "interpret"
ballarin@15598:     "interpretation"
wenzelm@12176:     "judgment"
wenzelm@12176:     "kill"
wenzelm@12176:     "kill_thy"
wenzelm@12176:     "lemma"
wenzelm@12176:     "lemmas"
wenzelm@12176:     "let"
wenzelm@27538:     "linear_undo"
wenzelm@30463:     "local_setup"
wenzelm@12176:     "locale"
wenzelm@49571:     "locale_deps"
wenzelm@12176:     "method_setup"
wenzelm@12176:     "moreover"
wenzelm@12176:     "next"
wenzelm@24945:     "no_notation"
wenzelm@15762:     "no_syntax"
wenzelm@19255:     "no_translations"
wenzelm@35414:     "no_type_notation"
wenzelm@41229:     "nonterminal"
wenzelm@21203:     "notation"
wenzelm@12176:     "note"
wenzelm@40960:     "notepad"
wenzelm@12176:     "obtain"
wenzelm@12176:     "oops"
wenzelm@12176:     "oracle"
haftmann@25516:     "overloading"
wenzelm@12176:     "parse_ast_translation"
wenzelm@12176:     "parse_translation"
wenzelm@12176:     "pr"
wenzelm@12176:     "prefer"
wenzelm@12176:     "presume"
wenzelm@12176:     "pretty_setmargin"
wenzelm@12176:     "prf"
bulwahn@31107:     "primrec"
wenzelm@56069:     "print_ML_antiquotations"
wenzelm@21732:     "print_abbrevs"
wenzelm@12176:     "print_antiquotations"
wenzelm@12176:     "print_ast_translation"
wenzelm@12176:     "print_attributes"
wenzelm@12176:     "print_binds"
wenzelm@47057:     "print_bundles"
wenzelm@12176:     "print_cases"
wenzelm@12176:     "print_claset"
haftmann@20378:     "print_classes"
haftmann@22288:     "print_codesetup"
wenzelm@12176:     "print_commands"
wenzelm@12176:     "print_context"
wenzelm@51585:     "print_defn_rules"
ballarin@41435:     "print_dependencies"
wenzelm@12176:     "print_facts"
wenzelm@12176:     "print_induct_rules"
ballarin@32804:     "print_interps"
wenzelm@12176:     "print_locale"
wenzelm@12176:     "print_locales"
wenzelm@12176:     "print_methods"
wenzelm@52060:     "print_options"
wenzelm@12365:     "print_rules"
wenzelm@12176:     "print_simpset"
wenzelm@52430:     "print_state"
wenzelm@19272:     "print_statement"
wenzelm@12176:     "print_syntax"
bulwahn@31107:     "print_tcset"
wenzelm@12176:     "print_theorems"
wenzelm@12176:     "print_theory"
wenzelm@12176:     "print_trans_rules"
wenzelm@12176:     "print_translation"
wenzelm@12176:     "proof"
wenzelm@12176:     "prop"
wenzelm@12176:     "pwd"
wenzelm@12176:     "qed"
wenzelm@12176:     "quit"
berghofe@13407:     "realizability"
berghofe@13407:     "realizers"
wenzelm@12176:     "remove_thy"
bulwahn@31107:     "rep_datatype"
wenzelm@36321:     "schematic_corollary"
wenzelm@36321:     "schematic_lemma"
wenzelm@36321:     "schematic_theorem"
wenzelm@12176:     "sect"
wenzelm@12176:     "section"
wenzelm@12176:     "setup"
wenzelm@12176:     "show"
wenzelm@22200:     "simproc_setup"
wenzelm@12176:     "sorry"
haftmann@24919:     "subclass"
ballarin@28895:     "sublocale"
wenzelm@12176:     "subsect"
wenzelm@12176:     "subsection"
wenzelm@12176:     "subsubsect"
wenzelm@12176:     "subsubsection"
wenzelm@12176:     "syntax"
wenzelm@40784:     "syntax_declaration"
wenzelm@12176:     "term"
wenzelm@12176:     "text"
wenzelm@12176:     "text_raw"
wenzelm@12176:     "then"
wenzelm@12176:     "theorem"
wenzelm@12176:     "theorems"
wenzelm@12176:     "theory"
wenzelm@12176:     "thm"
wenzelm@12176:     "thm_deps"
wenzelm@12176:     "thus"
haftmann@22486:     "thy_deps"
wenzelm@12176:     "translations"
wenzelm@12176:     "txt"
wenzelm@12176:     "txt_raw"
wenzelm@12176:     "typ"
wenzelm@35414:     "type_notation"
wenzelm@41249:     "type_synonym"
wenzelm@12176:     "typed_print_translation"
wenzelm@12176:     "typedecl"
wenzelm@12176:     "ultimately"
wenzelm@12176:     "undo"
wenzelm@12176:     "undos_proof"
wenzelm@18541:     "unfolding"
berghofe@26184:     "unused_thms"
wenzelm@12176:     "use_thy"
wenzelm@12926:     "using"
wenzelm@12176:     "welcome"
wenzelm@12176:     "with"
wenzelm@36505:     "write"
wenzelm@12176:     "{"
wenzelm@12176:     "}"))
wenzelm@12176: 
wenzelm@12176: (defconst isar-keywords-minor
wenzelm@52143:   '("and"
wenzelm@12176:     "assumes"
berghofe@17147:     "attach"
nipkow@15135:     "begin"
wenzelm@12176:     "binder"
bulwahn@31107:     "case_eqns"
bulwahn@31107:     "con_defs"
ballarin@16168:     "constrains"
wenzelm@12176:     "defines"
bulwahn@31107:     "domains"
bulwahn@31107:     "elimination"
wenzelm@12176:     "fixes"
wenzelm@19797:     "for"
haftmann@22288:     "identifier"
wenzelm@19797:     "if"
nipkow@15141:     "imports"
wenzelm@12176:     "in"
wenzelm@47069:     "includes"
bulwahn@31107:     "induction"
wenzelm@12176:     "infix"
wenzelm@12176:     "infixl"
wenzelm@12176:     "infixr"
bulwahn@31107:     "intros"
wenzelm@12176:     "is"
wenzelm@46938:     "keywords"
bulwahn@31107:     "monos"
wenzelm@12176:     "notes"
wenzelm@18888:     "obtains"
wenzelm@13364:     "open"
wenzelm@12176:     "output"
wenzelm@12176:     "overloaded"
wenzelm@33685:     "pervasive"
bulwahn@31107:     "recursor_eqns"
wenzelm@12935:     "shows"
wenzelm@12176:     "structure"
bulwahn@31107:     "type_elims"
bulwahn@31107:     "type_intros"
wenzelm@19633:     "unchecked"
wenzelm@12176:     "where"))
wenzelm@12176: 
wenzelm@12176: (defconst isar-keywords-control
wenzelm@25577:   '("Isabelle\\.command"
wenzelm@25577:     "ProofGeneral\\.inform_file_processed"
wenzelm@12176:     "ProofGeneral\\.inform_file_retracted"
wenzelm@12176:     "ProofGeneral\\.kill_proof"
wenzelm@52437:     "ProofGeneral\\.pr"
wenzelm@14937:     "ProofGeneral\\.process_pgip"
wenzelm@12176:     "ProofGeneral\\.restart"
wenzelm@12176:     "ProofGeneral\\.undo"
wenzelm@12176:     "cannot_undo"
wenzelm@40396:     "cd"
wenzelm@40396:     "commit"
wenzelm@37987:     "disable_pr"
wenzelm@37987:     "enable_pr"
wenzelm@12176:     "exit"
wenzelm@12176:     "init_toplevel"
wenzelm@12176:     "kill"
wenzelm@37987:     "kill_thy"
wenzelm@27538:     "linear_undo"
wenzelm@51270:     "pretty_setmargin"
wenzelm@12176:     "quit"
wenzelm@37987:     "remove_thy"
wenzelm@12176:     "undo"
wenzelm@37987:     "undos_proof"
wenzelm@37987:     "use_thy"))
wenzelm@12176: 
wenzelm@12176: (defconst isar-keywords-diag
wenzelm@26482:   '("ML_command"
wenzelm@26394:     "ML_val"
wenzelm@20568:     "class_deps"
wenzelm@14937:     "display_drafts"
kleing@29882:     "find_consts"
wenzelm@17220:     "find_theorems"
wenzelm@12176:     "full_prf"
wenzelm@12176:     "header"
wenzelm@21732:     "help"
wenzelm@49571:     "locale_deps"
wenzelm@52438:     "pr"
wenzelm@12176:     "prf"
wenzelm@56069:     "print_ML_antiquotations"
wenzelm@21732:     "print_abbrevs"
wenzelm@12176:     "print_antiquotations"
wenzelm@12176:     "print_attributes"
wenzelm@12176:     "print_binds"
wenzelm@47057:     "print_bundles"
wenzelm@12176:     "print_cases"
wenzelm@12176:     "print_claset"
haftmann@20378:     "print_classes"
haftmann@22288:     "print_codesetup"
wenzelm@12176:     "print_commands"
wenzelm@12176:     "print_context"
wenzelm@51585:     "print_defn_rules"
ballarin@41435:     "print_dependencies"
wenzelm@12176:     "print_facts"
wenzelm@12176:     "print_induct_rules"
ballarin@32804:     "print_interps"
wenzelm@12176:     "print_locale"
wenzelm@12176:     "print_locales"
wenzelm@12176:     "print_methods"
wenzelm@52060:     "print_options"
wenzelm@12365:     "print_rules"
wenzelm@12176:     "print_simpset"
wenzelm@52430:     "print_state"
wenzelm@19272:     "print_statement"
wenzelm@12176:     "print_syntax"
bulwahn@31107:     "print_tcset"
wenzelm@12176:     "print_theorems"
wenzelm@12176:     "print_theory"
wenzelm@12176:     "print_trans_rules"
wenzelm@12176:     "prop"
wenzelm@12176:     "pwd"
wenzelm@12176:     "term"
wenzelm@12176:     "thm"
wenzelm@12176:     "thm_deps"
haftmann@22486:     "thy_deps"
wenzelm@12176:     "typ"
berghofe@26184:     "unused_thms"
wenzelm@12176:     "welcome"))
wenzelm@12176: 
wenzelm@12176: (defconst isar-keywords-theory-begin
wenzelm@12176:   '("theory"))
wenzelm@12176: 
wenzelm@12176: (defconst isar-keywords-theory-switch
wenzelm@21302:   '())
wenzelm@12176: 
wenzelm@12176: (defconst isar-keywords-theory-end
wenzelm@12176:   '("end"))
wenzelm@12176: 
wenzelm@12176: (defconst isar-keywords-theory-heading
wenzelm@12176:   '("chapter"
wenzelm@12176:     "section"
wenzelm@12176:     "subsection"
wenzelm@12176:     "subsubsection"))
wenzelm@12176: 
wenzelm@12176: (defconst isar-keywords-theory-decl
wenzelm@26482:   '("ML"
wenzelm@48867:     "ML_file"
wenzelm@19069:     "abbreviation"
wenzelm@30527:     "attribute_setup"
haftmann@18702:     "axiomatization"
wenzelm@47057:     "bundle"
haftmann@18552:     "class"
bulwahn@31107:     "codatatype"
haftmann@22486:     "code_datatype"
bulwahn@31107:     "coinductive"
wenzelm@12176:     "consts"
wenzelm@21302:     "context"
bulwahn@31107:     "datatype"
wenzelm@22084:     "declaration"
wenzelm@23804:     "declare"
wenzelm@36455:     "default_sort"
wenzelm@18775:     "definition"
wenzelm@12176:     "defs"
berghofe@13407:     "extract"
berghofe@13407:     "extract_type"
wenzelm@36180:     "hide_class"
wenzelm@36180:     "hide_const"
wenzelm@36180:     "hide_fact"
wenzelm@36180:     "hide_type"
bulwahn@31107:     "inductive"
wenzelm@24866:     "instantiation"
wenzelm@12176:     "judgment"
wenzelm@12176:     "lemmas"
wenzelm@30463:     "local_setup"
wenzelm@12176:     "locale"
wenzelm@12176:     "method_setup"
wenzelm@24945:     "no_notation"
wenzelm@15762:     "no_syntax"
wenzelm@19255:     "no_translations"
wenzelm@35414:     "no_type_notation"
wenzelm@41229:     "nonterminal"
wenzelm@21203:     "notation"
wenzelm@40960:     "notepad"
wenzelm@12176:     "oracle"
haftmann@25516:     "overloading"
wenzelm@12176:     "parse_ast_translation"
wenzelm@12176:     "parse_translation"
bulwahn@31107:     "primrec"
wenzelm@12176:     "print_ast_translation"
wenzelm@12176:     "print_translation"
berghofe@13407:     "realizability"
berghofe@13407:     "realizers"
bulwahn@31107:     "rep_datatype"
wenzelm@12176:     "setup"
wenzelm@22200:     "simproc_setup"
wenzelm@12176:     "syntax"
wenzelm@40784:     "syntax_declaration"
wenzelm@12176:     "text"
wenzelm@12176:     "text_raw"
wenzelm@12176:     "theorems"
wenzelm@12176:     "translations"
wenzelm@35414:     "type_notation"
wenzelm@41249:     "type_synonym"
wenzelm@12176:     "typed_print_translation"
wenzelm@51295:     "typedecl"))
wenzelm@12176: 
wenzelm@12176: (defconst isar-keywords-theory-script
bulwahn@31107:   '("inductive_cases"))
wenzelm@12176: 
wenzelm@12176: (defconst isar-keywords-theory-goal
haftmann@36114:   '("corollary"
wenzelm@12176:     "instance"
ballarin@15598:     "interpretation"
wenzelm@12176:     "lemma"
wenzelm@36321:     "schematic_corollary"
wenzelm@36321:     "schematic_lemma"
wenzelm@36321:     "schematic_theorem"
haftmann@24919:     "subclass"
ballarin@28895:     "sublocale"
wenzelm@12176:     "theorem"))
wenzelm@12176: 
wenzelm@12176: (defconst isar-keywords-qed
wenzelm@12176:   '("\\."
wenzelm@12176:     "\\.\\."
wenzelm@12176:     "by"
wenzelm@12176:     "done"
wenzelm@12176:     "sorry"))
wenzelm@12176: 
wenzelm@12176: (defconst isar-keywords-qed-block
wenzelm@12176:   '("qed"))
wenzelm@12176: 
wenzelm@12176: (defconst isar-keywords-qed-global
wenzelm@12176:   '("oops"))
wenzelm@12176: 
wenzelm@12176: (defconst isar-keywords-proof-heading
wenzelm@12176:   '("sect"
wenzelm@12176:     "subsect"
wenzelm@12176:     "subsubsect"))
wenzelm@12176: 
wenzelm@12176: (defconst isar-keywords-proof-goal
wenzelm@12176:   '("have"
wenzelm@12176:     "hence"
wenzelm@29607:     "interpret"))
wenzelm@12176: 
wenzelm@12176: (defconst isar-keywords-proof-block
wenzelm@12176:   '("next"
wenzelm@12176:     "proof"))
wenzelm@12176: 
wenzelm@12176: (defconst isar-keywords-proof-open
wenzelm@12176:   '("{"))
wenzelm@12176: 
wenzelm@12176: (defconst isar-keywords-proof-close
wenzelm@12176:   '("}"))
wenzelm@12176: 
wenzelm@12176: (defconst isar-keywords-proof-chain
wenzelm@12176:   '("finally"
wenzelm@12176:     "from"
wenzelm@12176:     "then"
wenzelm@12176:     "ultimately"
wenzelm@12176:     "with"))
wenzelm@12176: 
wenzelm@12176: (defconst isar-keywords-proof-decl
wenzelm@28261:   '("ML_prf"
wenzelm@28261:     "also"
wenzelm@47057:     "include"
wenzelm@47057:     "including"
wenzelm@12176:     "let"
wenzelm@12176:     "moreover"
wenzelm@12176:     "note"
wenzelm@12176:     "txt"
wenzelm@12926:     "txt_raw"
wenzelm@18541:     "unfolding"
wenzelm@36505:     "using"
wenzelm@36505:     "write"))
wenzelm@12176: 
wenzelm@12176: (defconst isar-keywords-proof-asm
wenzelm@12176:   '("assume"
wenzelm@12176:     "case"
wenzelm@12176:     "def"
wenzelm@12176:     "fix"
wenzelm@12176:     "presume"))
wenzelm@12176: 
wenzelm@12176: (defconst isar-keywords-proof-asm-goal
wenzelm@17850:   '("guess"
wenzelm@21806:     "obtain"
wenzelm@21806:     "show"
wenzelm@21806:     "thus"))
wenzelm@12176: 
wenzelm@12176: (defconst isar-keywords-proof-script
wenzelm@12176:   '("apply"
wenzelm@12176:     "apply_end"
wenzelm@12176:     "back"
wenzelm@12176:     "defer"
wenzelm@12176:     "prefer"))
wenzelm@12176: 
wenzelm@12176: (provide 'isar-keywords)