etc/isar-keywords-ZF.el
author wenzelm
Mon, 31 Mar 2014 12:35:39 +0200
changeset 56334 6b3739fee456
parent 56275 600f432ab556
child 56618 874bdedb2313
permissions -rw-r--r--
some shortcuts for chunks, which sometimes avoid bulky string output;

;;
;; Keyword classification tables for Isabelle/Isar.
;; Generated from Pure + ZF.
;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***
;;

(defconst isar-keywords-major
  '("\\."
    "\\.\\."
    "Isabelle\\.command"
    "ML"
    "ML_command"
    "ML_file"
    "ML_prf"
    "ML_val"
    "ProofGeneral\\.inform_file_processed"
    "ProofGeneral\\.inform_file_retracted"
    "ProofGeneral\\.kill_proof"
    "ProofGeneral\\.pr"
    "ProofGeneral\\.process_pgip"
    "ProofGeneral\\.restart"
    "ProofGeneral\\.undo"
    "SML_file"
    "abbreviation"
    "also"
    "apply"
    "apply_end"
    "assume"
    "attribute_setup"
    "axiomatization"
    "back"
    "bundle"
    "by"
    "cannot_undo"
    "case"
    "cd"
    "chapter"
    "class"
    "class_deps"
    "codatatype"
    "code_datatype"
    "coinductive"
    "commit"
    "consts"
    "context"
    "corollary"
    "datatype"
    "declaration"
    "declare"
    "def"
    "default_sort"
    "defer"
    "definition"
    "defs"
    "disable_pr"
    "display_drafts"
    "done"
    "enable_pr"
    "end"
    "exit"
    "extract"
    "extract_type"
    "finally"
    "find_consts"
    "find_theorems"
    "fix"
    "from"
    "full_prf"
    "guess"
    "have"
    "header"
    "help"
    "hence"
    "hide_class"
    "hide_const"
    "hide_fact"
    "hide_type"
    "include"
    "including"
    "inductive"
    "inductive_cases"
    "init_toplevel"
    "instance"
    "instantiation"
    "interpret"
    "interpretation"
    "judgment"
    "kill"
    "kill_thy"
    "lemma"
    "lemmas"
    "let"
    "linear_undo"
    "local_setup"
    "locale"
    "locale_deps"
    "method_setup"
    "moreover"
    "next"
    "no_notation"
    "no_syntax"
    "no_translations"
    "no_type_notation"
    "nonterminal"
    "notation"
    "note"
    "notepad"
    "obtain"
    "oops"
    "oracle"
    "overloading"
    "parse_ast_translation"
    "parse_translation"
    "pr"
    "prefer"
    "presume"
    "pretty_setmargin"
    "prf"
    "primrec"
    "print_ML_antiquotations"
    "print_abbrevs"
    "print_antiquotations"
    "print_ast_translation"
    "print_attributes"
    "print_binds"
    "print_bundles"
    "print_cases"
    "print_claset"
    "print_classes"
    "print_codesetup"
    "print_commands"
    "print_context"
    "print_defn_rules"
    "print_dependencies"
    "print_facts"
    "print_induct_rules"
    "print_interps"
    "print_locale"
    "print_locales"
    "print_methods"
    "print_options"
    "print_rules"
    "print_simpset"
    "print_state"
    "print_statement"
    "print_syntax"
    "print_tcset"
    "print_theorems"
    "print_theory"
    "print_trans_rules"
    "print_translation"
    "proof"
    "prop"
    "pwd"
    "qed"
    "quit"
    "realizability"
    "realizers"
    "remove_thy"
    "rep_datatype"
    "schematic_corollary"
    "schematic_lemma"
    "schematic_theorem"
    "sect"
    "section"
    "setup"
    "show"
    "simproc_setup"
    "sorry"
    "subclass"
    "sublocale"
    "subsect"
    "subsection"
    "subsubsect"
    "subsubsection"
    "syntax"
    "syntax_declaration"
    "term"
    "text"
    "text_raw"
    "then"
    "theorem"
    "theorems"
    "theory"
    "thm"
    "thm_deps"
    "thus"
    "thy_deps"
    "translations"
    "txt"
    "txt_raw"
    "typ"
    "type_notation"
    "type_synonym"
    "typed_print_translation"
    "typedecl"
    "ultimately"
    "undo"
    "undos_proof"
    "unfolding"
    "unused_thms"
    "use_thy"
    "using"
    "welcome"
    "with"
    "write"
    "{"
    "}"))

(defconst isar-keywords-minor
  '("and"
    "assumes"
    "attach"
    "begin"
    "binder"
    "case_eqns"
    "con_defs"
    "constrains"
    "defines"
    "domains"
    "elimination"
    "fixes"
    "for"
    "identifier"
    "if"
    "imports"
    "in"
    "includes"
    "induction"
    "infix"
    "infixl"
    "infixr"
    "intros"
    "is"
    "keywords"
    "monos"
    "notes"
    "obtains"
    "open"
    "output"
    "overloaded"
    "pervasive"
    "recursor_eqns"
    "shows"
    "structure"
    "type_elims"
    "type_intros"
    "unchecked"
    "where"))

(defconst isar-keywords-control
  '("Isabelle\\.command"
    "ProofGeneral\\.inform_file_processed"
    "ProofGeneral\\.inform_file_retracted"
    "ProofGeneral\\.kill_proof"
    "ProofGeneral\\.pr"
    "ProofGeneral\\.process_pgip"
    "ProofGeneral\\.restart"
    "ProofGeneral\\.undo"
    "cannot_undo"
    "cd"
    "commit"
    "disable_pr"
    "enable_pr"
    "exit"
    "init_toplevel"
    "kill"
    "kill_thy"
    "linear_undo"
    "pretty_setmargin"
    "quit"
    "remove_thy"
    "undo"
    "undos_proof"
    "use_thy"))

(defconst isar-keywords-diag
  '("ML_command"
    "ML_val"
    "class_deps"
    "display_drafts"
    "find_consts"
    "find_theorems"
    "full_prf"
    "header"
    "help"
    "locale_deps"
    "pr"
    "prf"
    "print_ML_antiquotations"
    "print_abbrevs"
    "print_antiquotations"
    "print_attributes"
    "print_binds"
    "print_bundles"
    "print_cases"
    "print_claset"
    "print_classes"
    "print_codesetup"
    "print_commands"
    "print_context"
    "print_defn_rules"
    "print_dependencies"
    "print_facts"
    "print_induct_rules"
    "print_interps"
    "print_locale"
    "print_locales"
    "print_methods"
    "print_options"
    "print_rules"
    "print_simpset"
    "print_state"
    "print_statement"
    "print_syntax"
    "print_tcset"
    "print_theorems"
    "print_theory"
    "print_trans_rules"
    "prop"
    "pwd"
    "term"
    "thm"
    "thm_deps"
    "thy_deps"
    "typ"
    "unused_thms"
    "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"
    "ML_file"
    "SML_file"
    "abbreviation"
    "attribute_setup"
    "axiomatization"
    "bundle"
    "class"
    "codatatype"
    "code_datatype"
    "coinductive"
    "consts"
    "context"
    "datatype"
    "declaration"
    "declare"
    "default_sort"
    "definition"
    "defs"
    "extract"
    "extract_type"
    "hide_class"
    "hide_const"
    "hide_fact"
    "hide_type"
    "inductive"
    "inductive_cases"
    "instantiation"
    "judgment"
    "lemmas"
    "local_setup"
    "locale"
    "method_setup"
    "no_notation"
    "no_syntax"
    "no_translations"
    "no_type_notation"
    "nonterminal"
    "notation"
    "notepad"
    "oracle"
    "overloading"
    "parse_ast_translation"
    "parse_translation"
    "primrec"
    "print_ast_translation"
    "print_translation"
    "realizability"
    "realizers"
    "rep_datatype"
    "setup"
    "simproc_setup"
    "syntax"
    "syntax_declaration"
    "text"
    "text_raw"
    "theorems"
    "translations"
    "type_notation"
    "type_synonym"
    "typed_print_translation"
    "typedecl"))

(defconst isar-keywords-theory-script
  '())

(defconst isar-keywords-theory-goal
  '("corollary"
    "instance"
    "interpretation"
    "lemma"
    "schematic_corollary"
    "schematic_lemma"
    "schematic_theorem"
    "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"
    "include"
    "including"
    "let"
    "moreover"
    "note"
    "txt"
    "txt_raw"
    "unfolding"
    "using"
    "write"))

(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)