New files.

1 files changed, 486 insertions, 0 deletions

diff --git a/isar/isar-keywords.el b/isar/isar-keywords.el
new file mode 100644
index 00000000..1febdbf9
--- /dev/null
+++ b/isar/isar-keywords.el
@@ -0,0 +1,486 @@
+;;
+;; Keyword classification tables for Isabelle/Isar.
+;; This file was generated by Isabelle/HOLCF/IOA -- DO NOT EDIT!
+;;
+;; $Id$
+;;
+
+(defconst isar-keywords-major
+  '("\\."
+    "\\.\\."
+    "ML"
+    "ML_command"
+    "ML_setup"
+    "ProofGeneral\\.call_atp"
+    "ProofGeneral\\.context_thy_only"
+    "ProofGeneral\\.inform_file_processed"
+    "ProofGeneral\\.inform_file_retracted"
+    "ProofGeneral\\.kill_proof"
+    "ProofGeneral\\.process_pgip"
+    "ProofGeneral\\.redo"
+    "ProofGeneral\\.restart"
+    "ProofGeneral\\.try_context_thy_only"
+    "ProofGeneral\\.undo"
+    "also"
+    "apply"
+    "apply_end"
+    "arities"
+    "assume"
+    "automaton"
+    "ax_specification"
+    "axclass"
+    "axioms"
+    "back"
+    "by"
+    "cannot_undo"
+    "case"
+    "cd"
+    "chapter"
+    "classes"
+    "classrel"
+    "clear_undos"
+    "coinductive"
+    "commit"
+    "constdefs"
+    "consts"
+    "consts_code"
+    "context"
+    "corollary"
+    "cpodef"
+    "datatype"
+    "declare"
+    "def"
+    "defaultsort"
+    "defer"
+    "defer_recdef"
+    "defs"
+    "disable_pr"
+    "display_drafts"
+    "domain"
+    "done"
+    "enable_pr"
+    "end"
+    "exit"
+    "extract"
+    "extract_type"
+    "finalconsts"
+    "finally"
+    "fix"
+    "fixpat"
+    "fixrec"
+    "from"
+    "full_prf"
+    "generate_code"
+    "global"
+    "have"
+    "header"
+    "hence"
+    "hide"
+    "inductive"
+    "inductive_cases"
+    "init_toplevel"
+    "instance"
+    "interpret"
+    "interpretation"
+    "judgment"
+    "kill"
+    "kill_thy"
+    "lemma"
+    "lemmas"
+    "let"
+    "local"
+    "locale"
+    "method_setup"
+    "moreover"
+    "next"
+    "no_syntax"
+    "nonterminals"
+    "note"
+    "obtain"
+    "oops"
+    "oracle"
+    "parse_ast_translation"
+    "parse_translation"
+    "pcpodef"
+    "pr"
+    "prefer"
+    "presume"
+    "pretty_setmargin"
+    "prf"
+    "primrec"
+    "print_antiquotations"
+    "print_ast_translation"
+    "print_attributes"
+    "print_binds"
+    "print_cases"
+    "print_claset"
+    "print_commands"
+    "print_context"
+    "print_drafts"
+    "print_facts"
+    "print_induct_rules"
+    "print_interps"
+    "print_locale"
+    "print_locales"
+    "print_methods"
+    "print_rules"
+    "print_simpset"
+    "print_syntax"
+    "print_theorems"
+    "print_theory"
+    "print_trans_rules"
+    "print_translation"
+    "proof"
+    "prop"
+    "pwd"
+    "qed"
+    "quickcheck"
+    "quickcheck_params"
+    "quit"
+    "realizability"
+    "realizers"
+    "recdef"
+    "recdef_tc"
+    "record"
+    "redo"
+    "refute"
+    "refute_params"
+    "remove_thy"
+    "rep_datatype"
+    "sect"
+    "section"
+    "setup"
+    "show"
+    "sorry"
+    "specification"
+    "subsect"
+    "subsection"
+    "subsubsect"
+    "subsubsection"
+    "syntax"
+    "term"
+    "text"
+    "text_raw"
+    "then"
+    "theorem"
+    "theorems"
+    "theory"
+    "thm"
+    "thm_deps"
+    "thms_containing"
+    "thus"
+    "token_translation"
+    "touch_all_thys"
+    "touch_child_thys"
+    "touch_thy"
+    "translations"
+    "txt"
+    "txt_raw"
+    "typ"
+    "typed_print_translation"
+    "typedecl"
+    "typedef"
+    "types"
+    "types_code"
+    "ultimately"
+    "undo"
+    "undos_proof"
+    "update_thy"
+    "update_thy_only"
+    "use"
+    "use_thy"
+    "use_thy_only"
+    "using"
+    "welcome"
+    "with"
+    "{"
+    "}"))
+
+(defconst isar-keywords-minor
+  '("actions"
+    "advanced"
+    "and"
+    "assumes"
+    "attach"
+    "begin"
+    "binder"
+    "compose"
+    "concl"
+    "congs"
+    "constrains"
+    "defines"
+    "distinct"
+    "files"
+    "fixes"
+    "hide_action"
+    "hints"
+    "imports"
+    "in"
+    "includes"
+    "induction"
+    "infix"
+    "infixl"
+    "infixr"
+    "initially"
+    "inject"
+    "inputs"
+    "internals"
+    "intros"
+    "is"
+    "lazy"
+    "monos"
+    "morphisms"
+    "notes"
+    "open"
+    "output"
+    "outputs"
+    "overloaded"
+    "permissive"
+    "post"
+    "pre"
+    "rename"
+    "restrict"
+    "shows"
+    "signature"
+    "states"
+    "structure"
+    "to"
+    "transitions"
+    "transrel"
+    "uses"
+    "where"))
+
+(defconst isar-keywords-control
+  '("ProofGeneral\\.context_thy_only"
+    "ProofGeneral\\.inform_file_processed"
+    "ProofGeneral\\.inform_file_retracted"
+    "ProofGeneral\\.kill_proof"
+    "ProofGeneral\\.process_pgip"
+    "ProofGeneral\\.redo"
+    "ProofGeneral\\.restart"
+    "ProofGeneral\\.try_context_thy_only"
+    "ProofGeneral\\.undo"
+    "cannot_undo"
+    "clear_undos"
+    "exit"
+    "init_toplevel"
+    "kill"
+    "quit"
+    "redo"
+    "undo"
+    "undos_proof"))
+
+(defconst isar-keywords-diag
+  '("ML"
+    "ML_command"
+    "ProofGeneral\\.call_atp"
+    "cd"
+    "commit"
+    "disable_pr"
+    "display_drafts"
+    "enable_pr"
+    "full_prf"
+    "header"
+    "kill_thy"
+    "pr"
+    "pretty_setmargin"
+    "prf"
+    "print_antiquotations"
+    "print_attributes"
+    "print_binds"
+    "print_cases"
+    "print_claset"
+    "print_commands"
+    "print_context"
+    "print_drafts"
+    "print_facts"
+    "print_induct_rules"
+    "print_interps"
+    "print_locale"
+    "print_locales"
+    "print_methods"
+    "print_rules"
+    "print_simpset"
+    "print_syntax"
+    "print_theorems"
+    "print_theory"
+    "print_trans_rules"
+    "prop"
+    "pwd"
+    "quickcheck"
+    "refute"
+    "remove_thy"
+    "term"
+    "thm"
+    "thm_deps"
+    "thms_containing"
+    "touch_all_thys"
+    "touch_child_thys"
+    "touch_thy"
+    "typ"
+    "update_thy"
+    "update_thy_only"
+    "use"
+    "use_thy"
+    "use_thy_only"
+    "welcome"))
+
+(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"))
+
+(defconst isar-keywords-theory-decl
+  '("ML_setup"
+    "arities"
+    "automaton"
+    "axclass"
+    "axioms"
+    "classes"
+    "classrel"
+    "coinductive"
+    "constdefs"
+    "consts"
+    "consts_code"
+    "datatype"
+    "defaultsort"
+    "defer_recdef"
+    "defs"
+    "domain"
+    "extract"
+    "extract_type"
+    "finalconsts"
+    "fixpat"
+    "fixrec"
+    "generate_code"
+    "global"
+    "hide"
+    "inductive"
+    "judgment"
+    "lemmas"
+    "local"
+    "locale"
+    "method_setup"
+    "no_syntax"
+    "nonterminals"
+    "oracle"
+    "parse_ast_translation"
+    "parse_translation"
+    "primrec"
+    "print_ast_translation"
+    "print_translation"
+    "quickcheck_params"
+    "realizability"
+    "realizers"
+    "recdef"
+    "record"
+    "refute_params"
+    "rep_datatype"
+    "setup"
+    "syntax"
+    "text"
+    "text_raw"
+    "theorems"
+    "token_translation"
+    "translations"
+    "typed_print_translation"
+    "typedecl"
+    "types"
+    "types_code"))
+
+(defconst isar-keywords-theory-script
+  '("declare"
+    "inductive_cases"))
+
+(defconst isar-keywords-theory-goal
+  '("ax_specification"
+    "corollary"
+    "cpodef"
+    "instance"
+    "interpretation"
+    "lemma"
+    "pcpodef"
+    "recdef_tc"
+    "specification"
+    "theorem"
+    "typedef"))
+
+(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"
+    "show"
+    "thus"))
+
+(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
+  '("also"
+    "let"
+    "moreover"
+    "note"
+    "txt"
+    "txt_raw"
+    "using"))
+
+(defconst isar-keywords-proof-asm
+  '("assume"
+    "case"
+    "def"
+    "fix"
+    "presume"))
+
+(defconst isar-keywords-proof-asm-goal
+  '("obtain"))
+
+(defconst isar-keywords-proof-script
+  '("apply"
+    "apply_end"
+    "back"
+    "defer"
+    "prefer"))
+
+(provide 'isar-keywords)