;;
;; Keyword classification tables for Isabelle/Isar.
;; This file generated by Isabelle -- DO NOT EDIT!
;;
;; $Id$
;;

(defconst isar-keywords-minor
  '("and"
    "as"
    "binder"
    "con_defs"
    "concl"
    "congs"
    "distinct"
    "files"
    "induction"
    "infixl"
    "infixr"
    "inject"
    "intrs"
    "is"
    "monos"
    "output"
    "simpset"))

(defconst isar-keywords-control
  '("cannot_undo"
    "cd"
    "clear_undo"
    "exit"
    "init_toplevel"
    "kill"
    "kill_proof"
    "quit"
    "redo"
    "undo"
    "undos_proof"))

(defconst isar-keywords-diag
  '("ML"
    "commit"
    "disable_pr"
    "enable_pr"
    "help"
    "pr"
    "pretty_setmargin"
    "print_attributes"
    "print_binds"
    "print_context"
    "print_facts"
    "print_methods"
    "print_syntax"
    "print_theorems"
    "print_theory"
    "prop"
    "pwd"
    "remove_thy"
    "term"
    "thm"
    "touch_all_thys"
    "touch_thy"
    "typ"
    "update_thy"
    "update_thy_only"
    "use"
    "use_thy"
    "use_thy_only"))

(defconst isar-keywords-theory-begin
  '("theory"))

(defconst isar-keywords-theory-switch
  '("context"))

(defconst isar-keywords-theory-end
  '("end"))

(defconst isar-keywords-theory-heading
  '("chapter"
    "section"
    "subsection"
    "subsubsection"
    "title"))

(defconst isar-keywords-theory-decl
  '("arities"
    "axclass"
    "axioms"
    "classes"
    "classrel"
    "coinductive"
    "constdefs"
    "consts"
    "datatype"
    "defaultsort"
    "defer_recdef"
    "defs"
    "global"
    "inductive"
    "inductive_cases"
    "lemmas"
    "local"
    "nonterminals"
    "oracle"
    "parse_ast_translation"
    "parse_translation"
    "primrec"
    "print_ast_translation"
    "print_translation"
    "recdef"
    "record"
    "rep_datatype"
    "setup"
    "syntax"
    "text"
    "theorems"
    "token_translation"
    "translations"
    "typed_print_translation"
    "typedecl"
    "types"))

(defconst isar-keywords-theory-goal
  '("instance"
    "lemma"
    "theorem"
    "typedef"))

(defconst isar-keywords-qed
  '("\\."
    "\\.\\."
    "by"
    "sorry"))

(defconst isar-keywords-qed-block
  '("qed"))

(defconst isar-keywords-proof-goal
  '("have"
    "hence"
    "show"
    "thus"))

(defconst isar-keywords-proof-block
  '("next"
    "proof"
    "{{"
    "}}"))

(defconst isar-keywords-proof-chain
  '("finally"
    "from"
    "then"
    "thence"
    "with"))

(defconst isar-keywords-proof-decl
  '("also"
    "let"
    "note"
    "sect"
    "subsect"
    "subsubsect"
    "txt"))

(defconst isar-keywords-proof-asm
  '("assume"
    "def"
    "fix"
    "presume"))

(defconst isar-keywords-proof-script
  '("apply"
    "back"
    "then_apply"))

(provide 'isar-keywords)