--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/etc/isar-keywords-HOL-Nominal.el Fri Apr 28 16:04:57 2006 +0200
@@ -0,0 +1,504 @@
+;;
+;; Keyword classification tables for Isabelle/Isar.
+;; This file was generated by Isabelle/HOL/HOL-Nominal -- 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"
+ "abbreviation"
+ "also"
+ "apply"
+ "apply_end"
+ "arities"
+ "assume"
+ "atom_decl"
+ "ax_specification"
+ "axclass"
+ "axiomatization"
+ "axioms"
+ "back"
+ "by"
+ "cannot_undo"
+ "case"
+ "cd"
+ "chapter"
+ "class"
+ "classes"
+ "classrel"
+ "clear_undos"
+ "code_alias"
+ "code_generate"
+ "code_library"
+ "code_module"
+ "code_primclass"
+ "code_primconst"
+ "code_primtyco"
+ "code_purge"
+ "code_serialize"
+ "code_syntax_const"
+ "code_syntax_tyco"
+ "coinductive"
+ "commit"
+ "constdefs"
+ "consts"
+ "consts_code"
+ "context"
+ "corollary"
+ "datatype"
+ "declare"
+ "def"
+ "defaultsort"
+ "defer"
+ "defer_recdef"
+ "definition"
+ "defs"
+ "disable_pr"
+ "display_drafts"
+ "done"
+ "enable_pr"
+ "end"
+ "exit"
+ "extract"
+ "extract_type"
+ "finalconsts"
+ "finally"
+ "find_theorems"
+ "fix"
+ "from"
+ "full_prf"
+ "global"
+ "guess"
+ "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"
+ "no_translations"
+ "nominal_datatype"
+ "nonterminals"
+ "norm_by_eval"
+ "note"
+ "obtain"
+ "oops"
+ "oracle"
+ "parse_ast_translation"
+ "parse_translation"
+ "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_statement"
+ "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"
+ "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"
+ "unfolding"
+ "update_thy"
+ "update_thy_only"
+ "use"
+ "use_thy"
+ "use_thy_only"
+ "using"
+ "value"
+ "welcome"
+ "with"
+ "{"
+ "}"))
+
+(defconst isar-keywords-minor
+ '("advanced"
+ "and"
+ "assumes"
+ "attach"
+ "begin"
+ "binder"
+ "concl"
+ "congs"
+ "constrains"
+ "contains"
+ "defines"
+ "distinct"
+ "file"
+ "fixes"
+ "hints"
+ "imports"
+ "in"
+ "includes"
+ "induction"
+ "infix"
+ "infixl"
+ "infixr"
+ "inject"
+ "intros"
+ "is"
+ "monos"
+ "morphisms"
+ "notes"
+ "obtains"
+ "open"
+ "output"
+ "overloaded"
+ "permissive"
+ "shows"
+ "structure"
+ "target_atom"
+ "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"
+ "find_theorems"
+ "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_statement"
+ "print_syntax"
+ "print_theorems"
+ "print_theory"
+ "print_trans_rules"
+ "prop"
+ "pwd"
+ "quickcheck"
+ "refute"
+ "remove_thy"
+ "term"
+ "thm"
+ "thm_deps"
+ "touch_all_thys"
+ "touch_child_thys"
+ "touch_thy"
+ "typ"
+ "update_thy"
+ "update_thy_only"
+ "use"
+ "use_thy"
+ "use_thy_only"
+ "value"
+ "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"
+ "abbreviation"
+ "arities"
+ "atom_decl"
+ "axclass"
+ "axiomatization"
+ "axioms"
+ "class"
+ "classes"
+ "classrel"
+ "code_alias"
+ "code_generate"
+ "code_library"
+ "code_module"
+ "code_primclass"
+ "code_primconst"
+ "code_primtyco"
+ "code_purge"
+ "code_serialize"
+ "code_syntax_const"
+ "code_syntax_tyco"
+ "coinductive"
+ "constdefs"
+ "consts"
+ "consts_code"
+ "datatype"
+ "defaultsort"
+ "defer_recdef"
+ "definition"
+ "defs"
+ "extract"
+ "extract_type"
+ "finalconsts"
+ "global"
+ "hide"
+ "inductive"
+ "judgment"
+ "lemmas"
+ "local"
+ "locale"
+ "method_setup"
+ "no_syntax"
+ "no_translations"
+ "nominal_datatype"
+ "nonterminals"
+ "norm_by_eval"
+ "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"
+ "instance"
+ "interpretation"
+ "lemma"
+ "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"
+ "unfolding"
+ "using"))
+
+(defconst isar-keywords-proof-asm
+ '("assume"
+ "case"
+ "def"
+ "fix"
+ "presume"))
+
+(defconst isar-keywords-proof-asm-goal
+ '("guess"
+ "obtain"))
+
+(defconst isar-keywords-proof-script
+ '("apply"
+ "apply_end"
+ "back"
+ "defer"
+ "prefer"))
+
+(provide 'isar-keywords)