wenzelm@12176: ;;
wenzelm@12176: ;; Keyword classification tables for Isabelle/Isar.
wenzelm@12176: ;; This file was generated by Isabelle/ZF -- DO NOT EDIT!
wenzelm@12176: ;;
wenzelm@12176: ;; $Id$
wenzelm@12176: ;;
wenzelm@12176: 
wenzelm@12176: (defconst isar-keywords-major
wenzelm@12176:   '("\\."
wenzelm@12176:     "\\.\\."
wenzelm@12176:     "ML"
wenzelm@12176:     "ML_command"
wenzelm@12176:     "ML_setup"
wenzelm@12176:     "ProofGeneral\\.context_thy_only"
wenzelm@12176:     "ProofGeneral\\.inform_file_processed"
wenzelm@12176:     "ProofGeneral\\.inform_file_retracted"
wenzelm@12176:     "ProofGeneral\\.kill_proof"
wenzelm@12176:     "ProofGeneral\\.restart"
wenzelm@12176:     "ProofGeneral\\.try_context_thy_only"
wenzelm@12176:     "ProofGeneral\\.undo"
wenzelm@12176:     "also"
wenzelm@12176:     "apply"
wenzelm@12176:     "apply_end"
wenzelm@12176:     "arities"
wenzelm@12176:     "assume"
wenzelm@12176:     "axclass"
wenzelm@12176:     "axioms"
wenzelm@12176:     "back"
wenzelm@12176:     "by"
wenzelm@12176:     "cannot_undo"
wenzelm@12176:     "case"
wenzelm@12176:     "cd"
wenzelm@12176:     "chapter"
wenzelm@12176:     "classes"
wenzelm@12176:     "classrel"
wenzelm@12176:     "clear_undos"
wenzelm@12179:     "codatatype"
wenzelm@12176:     "coinductive"
wenzelm@12176:     "commit"
wenzelm@12176:     "constdefs"
wenzelm@12176:     "consts"
wenzelm@12176:     "consts_code"
wenzelm@12176:     "context"
wenzelm@12176:     "corollary"
wenzelm@12179:     "datatype"
wenzelm@12176:     "declare"
wenzelm@12176:     "def"
wenzelm@12176:     "defaultsort"
wenzelm@12176:     "defer"
wenzelm@12176:     "defs"
wenzelm@12176:     "disable_pr"
wenzelm@12176:     "done"
wenzelm@12176:     "enable_pr"
wenzelm@12176:     "end"
wenzelm@12176:     "exit"
wenzelm@12176:     "finally"
wenzelm@12176:     "fix"
wenzelm@12176:     "from"
wenzelm@12176:     "full_prf"
wenzelm@12176:     "generate_code"
wenzelm@12176:     "global"
wenzelm@12176:     "have"
wenzelm@12176:     "header"
wenzelm@12176:     "hence"
wenzelm@12176:     "hide"
wenzelm@12176:     "inductive"
wenzelm@12176:     "inductive_cases"
wenzelm@12176:     "init_toplevel"
wenzelm@12176:     "instance"
wenzelm@12176:     "judgment"
wenzelm@12176:     "kill"
wenzelm@12176:     "kill_thy"
wenzelm@12176:     "lemma"
wenzelm@12176:     "lemmas"
wenzelm@12176:     "let"
wenzelm@12176:     "local"
wenzelm@12176:     "locale"
wenzelm@12176:     "method_setup"
wenzelm@12176:     "moreover"
wenzelm@12176:     "next"
wenzelm@12176:     "nonterminals"
wenzelm@12176:     "note"
wenzelm@12176:     "obtain"
wenzelm@12176:     "oops"
wenzelm@12176:     "oracle"
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"
wenzelm@12179:     "primrec"
wenzelm@12176:     "print_antiquotations"
wenzelm@12176:     "print_ast_translation"
wenzelm@12176:     "print_attributes"
wenzelm@12176:     "print_binds"
wenzelm@12176:     "print_cases"
wenzelm@12176:     "print_claset"
wenzelm@12176:     "print_commands"
wenzelm@12176:     "print_context"
wenzelm@12176:     "print_facts"
wenzelm@12176:     "print_induct_rules"
wenzelm@12176:     "print_locale"
wenzelm@12176:     "print_locales"
wenzelm@12176:     "print_methods"
wenzelm@12365:     "print_rules"
wenzelm@12176:     "print_simpset"
wenzelm@12176:     "print_syntax"
wenzelm@12184:     "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"
wenzelm@12176:     "redo"
wenzelm@12176:     "remove_thy"
wenzelm@12211:     "rep_datatype"
wenzelm@12176:     "sect"
wenzelm@12176:     "section"
wenzelm@12176:     "setup"
wenzelm@12176:     "show"
wenzelm@12176:     "sorry"
wenzelm@12176:     "subsect"
wenzelm@12176:     "subsection"
wenzelm@12176:     "subsubsect"
wenzelm@12176:     "subsubsection"
wenzelm@12176:     "syntax"
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:     "thms_containing"
wenzelm@12176:     "thus"
wenzelm@12176:     "token_translation"
wenzelm@12176:     "touch_all_thys"
wenzelm@12176:     "touch_child_thys"
wenzelm@12176:     "touch_thy"
wenzelm@12176:     "translations"
wenzelm@12176:     "txt"
wenzelm@12176:     "txt_raw"
wenzelm@12176:     "typ"
wenzelm@12176:     "typed_print_translation"
wenzelm@12176:     "typedecl"
wenzelm@12176:     "types"
wenzelm@12176:     "types_code"
wenzelm@12176:     "ultimately"
wenzelm@12176:     "undo"
wenzelm@12176:     "undos_proof"
wenzelm@12176:     "update_thy"
wenzelm@12176:     "update_thy_only"
wenzelm@12176:     "use"
wenzelm@12176:     "use_thy"
wenzelm@12176:     "use_thy_only"
wenzelm@12926:     "using"
wenzelm@12176:     "welcome"
wenzelm@12176:     "with"
wenzelm@12176:     "{"
wenzelm@12176:     "}"))
wenzelm@12176: 
wenzelm@12176: (defconst isar-keywords-minor
wenzelm@12176:   '("and"
wenzelm@12176:     "assumes"
wenzelm@12176:     "binder"
wenzelm@12211:     "case_eqns"
wenzelm@12176:     "con_defs"
wenzelm@12176:     "concl"
wenzelm@12176:     "defines"
wenzelm@12176:     "domains"
wenzelm@12211:     "elimination"
wenzelm@12176:     "files"
wenzelm@12176:     "fixes"
wenzelm@12176:     "in"
wenzelm@12211:     "induction"
wenzelm@12176:     "infix"
wenzelm@12176:     "infixl"
wenzelm@12176:     "infixr"
wenzelm@12176:     "intros"
wenzelm@12176:     "is"
wenzelm@12176:     "monos"
wenzelm@12176:     "notes"
wenzelm@12176:     "output"
wenzelm@12176:     "overloaded"
wenzelm@12211:     "recursor_eqns"
wenzelm@12176:     "structure"
wenzelm@12176:     "type_elims"
wenzelm@12176:     "type_intros"
wenzelm@12176:     "uses"
wenzelm@12176:     "where"))
wenzelm@12176: 
wenzelm@12176: (defconst isar-keywords-control
wenzelm@12176:   '("ProofGeneral\\.context_thy_only"
wenzelm@12176:     "ProofGeneral\\.inform_file_processed"
wenzelm@12176:     "ProofGeneral\\.inform_file_retracted"
wenzelm@12176:     "ProofGeneral\\.kill_proof"
wenzelm@12176:     "ProofGeneral\\.restart"
wenzelm@12176:     "ProofGeneral\\.try_context_thy_only"
wenzelm@12176:     "ProofGeneral\\.undo"
wenzelm@12176:     "cannot_undo"
wenzelm@12176:     "clear_undos"
wenzelm@12176:     "exit"
wenzelm@12176:     "init_toplevel"
wenzelm@12176:     "kill"
wenzelm@12176:     "quit"
wenzelm@12176:     "redo"
wenzelm@12176:     "undo"
wenzelm@12176:     "undos_proof"))
wenzelm@12176: 
wenzelm@12176: (defconst isar-keywords-diag
wenzelm@12176:   '("ML"
wenzelm@12176:     "ML_command"
wenzelm@12176:     "cd"
wenzelm@12176:     "commit"
wenzelm@12176:     "disable_pr"
wenzelm@12176:     "enable_pr"
wenzelm@12176:     "full_prf"
wenzelm@12176:     "header"
wenzelm@12176:     "kill_thy"
wenzelm@12176:     "pr"
wenzelm@12176:     "pretty_setmargin"
wenzelm@12176:     "prf"
wenzelm@12176:     "print_antiquotations"
wenzelm@12176:     "print_attributes"
wenzelm@12176:     "print_binds"
wenzelm@12176:     "print_cases"
wenzelm@12176:     "print_claset"
wenzelm@12176:     "print_commands"
wenzelm@12176:     "print_context"
wenzelm@12176:     "print_facts"
wenzelm@12176:     "print_induct_rules"
wenzelm@12176:     "print_locale"
wenzelm@12176:     "print_locales"
wenzelm@12176:     "print_methods"
wenzelm@12365:     "print_rules"
wenzelm@12176:     "print_simpset"
wenzelm@12176:     "print_syntax"
wenzelm@12184:     "print_tcset"
wenzelm@12176:     "print_theorems"
wenzelm@12176:     "print_theory"
wenzelm@12176:     "print_trans_rules"
wenzelm@12176:     "prop"
wenzelm@12176:     "pwd"
wenzelm@12176:     "remove_thy"
wenzelm@12176:     "term"
wenzelm@12176:     "thm"
wenzelm@12176:     "thm_deps"
wenzelm@12176:     "thms_containing"
wenzelm@12176:     "touch_all_thys"
wenzelm@12176:     "touch_child_thys"
wenzelm@12176:     "touch_thy"
wenzelm@12176:     "typ"
wenzelm@12176:     "update_thy"
wenzelm@12176:     "update_thy_only"
wenzelm@12176:     "use"
wenzelm@12176:     "use_thy"
wenzelm@12176:     "use_thy_only"
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@12176:   '("context"))
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@12176:   '("ML_setup"
wenzelm@12176:     "arities"
wenzelm@12176:     "axclass"
wenzelm@12176:     "axioms"
wenzelm@12176:     "classes"
wenzelm@12176:     "classrel"
wenzelm@12179:     "codatatype"
wenzelm@12176:     "coinductive"
wenzelm@12176:     "constdefs"
wenzelm@12176:     "consts"
wenzelm@12176:     "consts_code"
wenzelm@12179:     "datatype"
wenzelm@12176:     "defaultsort"
wenzelm@12176:     "defs"
wenzelm@12176:     "generate_code"
wenzelm@12176:     "global"
wenzelm@12176:     "hide"
wenzelm@12176:     "inductive"
wenzelm@12176:     "judgment"
wenzelm@12176:     "lemmas"
wenzelm@12176:     "local"
wenzelm@12176:     "locale"
wenzelm@12176:     "method_setup"
wenzelm@12176:     "nonterminals"
wenzelm@12176:     "oracle"
wenzelm@12176:     "parse_ast_translation"
wenzelm@12176:     "parse_translation"
wenzelm@12179:     "primrec"
wenzelm@12176:     "print_ast_translation"
wenzelm@12176:     "print_translation"
wenzelm@12211:     "rep_datatype"
wenzelm@12176:     "setup"
wenzelm@12176:     "syntax"
wenzelm@12176:     "text"
wenzelm@12176:     "text_raw"
wenzelm@12176:     "theorems"
wenzelm@12176:     "token_translation"
wenzelm@12176:     "translations"
wenzelm@12176:     "typed_print_translation"
wenzelm@12176:     "typedecl"
wenzelm@12176:     "types"
wenzelm@12176:     "types_code"))
wenzelm@12176: 
wenzelm@12176: (defconst isar-keywords-theory-script
wenzelm@12176:   '("declare"
wenzelm@12176:     "inductive_cases"))
wenzelm@12176: 
wenzelm@12176: (defconst isar-keywords-theory-goal
wenzelm@12176:   '("corollary"
wenzelm@12176:     "instance"
wenzelm@12176:     "lemma"
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@12176:     "show"
wenzelm@12176:     "thus"))
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@12176:   '("also"
wenzelm@12176:     "let"
wenzelm@12176:     "moreover"
wenzelm@12176:     "note"
wenzelm@12176:     "txt"
wenzelm@12926:     "txt_raw"
wenzelm@12926:     "using"))
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@12176:   '("obtain"))
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)