--- a/Admin/update-keywords Mon Oct 08 16:28:29 2007 +0200
+++ b/Admin/update-keywords Mon Oct 08 18:13:01 2007 +0200
@@ -14,10 +14,7 @@
cd "$ISABELLE_HOME/etc"
isatool keywords -t emacs \
- "$LOG/Pure.gz" "$LOG/Pure-ProofGeneral.gz" "$LOG/HOL.gz" "$LOG/HOLCF.gz" "$LOG/IOA.gz"
-
-isatool keywords -t emacs -k HOL-Nominal \
- "$LOG/Pure.gz" "$LOG/Pure-ProofGeneral.gz" "$LOG/HOL.gz" "$LOG/HOL-Nominal.gz"
+ "$LOG/Pure.gz" "$LOG/Pure-ProofGeneral.gz" "$LOG/HOL.gz" "$LOG/HOLCF.gz" "$LOG/IOA.gz" "$LOG/HOL-Nominal.gz"
isatool keywords -t emacs -k ZF \
"$LOG/Pure.gz" "$LOG/Pure-ProofGeneral.gz" "$LOG/FOL.gz" "$LOG/ZF.gz"
--- a/etc/isar-keywords-HOL-Nominal.el Mon Oct 08 16:28:29 2007 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,556 +0,0 @@
-;;
-;; Keyword classification tables for Isabelle/Isar.
-;; This file was generated from HOL + HOL-Nominal -- DO NOT EDIT!
-;;
-;; $Id$
-;;
-
-(defconst isar-keywords-major
- '("\\."
- "\\.\\."
- "ML"
- "ML_command"
- "ML_setup"
- "ProofGeneral\\.inform_file_processed"
- "ProofGeneral\\.inform_file_retracted"
- "ProofGeneral\\.kill_proof"
- "ProofGeneral\\.process_pgip"
- "ProofGeneral\\.restart"
- "ProofGeneral\\.undo"
- "abbreviation"
- "also"
- "apply"
- "apply_end"
- "arities"
- "assume"
- "atom_decl"
- "ax_specification"
- "axclass"
- "axiomatization"
- "axioms"
- "back"
- "by"
- "cannot_undo"
- "case"
- "cd"
- "chapter"
- "class"
- "class_deps"
- "classes"
- "classrel"
- "code_class"
- "code_const"
- "code_datatype"
- "code_deps"
- "code_exception"
- "code_instance"
- "code_library"
- "code_module"
- "code_modulename"
- "code_moduleprolog"
- "code_monad"
- "code_props"
- "code_reserved"
- "code_thms"
- "code_type"
- "coinductive"
- "coinductive_set"
- "commit"
- "constdefs"
- "consts"
- "consts_code"
- "context"
- "corollary"
- "datatype"
- "declaration"
- "declare"
- "def"
- "defaultsort"
- "defer"
- "defer_recdef"
- "definition"
- "defs"
- "disable_pr"
- "display_drafts"
- "done"
- "enable_pr"
- "end"
- "equivariance"
- "exit"
- "export_code"
- "extract"
- "extract_type"
- "finalconsts"
- "finally"
- "find_theorems"
- "fix"
- "from"
- "full_prf"
- "fun"
- "function"
- "global"
- "guess"
- "have"
- "header"
- "help"
- "hence"
- "hide"
- "inductive"
- "inductive_cases"
- "inductive_set"
- "init_toplevel"
- "instance"
- "instance_proof"
- "instantiation"
- "interpret"
- "interpretation"
- "invoke"
- "judgment"
- "kill"
- "kill_thy"
- "lemma"
- "lemmas"
- "let"
- "local"
- "locale"
- "method_setup"
- "moreover"
- "next"
- "no_syntax"
- "no_translations"
- "nominal_datatype"
- "nominal_inductive"
- "nominal_primrec"
- "nonterminals"
- "normal_form"
- "notation"
- "note"
- "obtain"
- "oops"
- "oracle"
- "parse_ast_translation"
- "parse_translation"
- "pr"
- "prefer"
- "presume"
- "pretty_setmargin"
- "prf"
- "primrec"
- "print_abbrevs"
- "print_antiquotations"
- "print_ast_translation"
- "print_atp_rules"
- "print_attributes"
- "print_binds"
- "print_cases"
- "print_claset"
- "print_classes"
- "print_codesetup"
- "print_commands"
- "print_configs"
- "print_context"
- "print_drafts"
- "print_facts"
- "print_induct_rules"
- "print_interps"
- "print_locale"
- "print_locales"
- "print_methods"
- "print_noatp_rules"
- "print_orders"
- "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"
- "simproc_setup"
- "sledgehammer"
- "sorry"
- "specification"
- "subsect"
- "subsection"
- "subsubsect"
- "subsubsection"
- "syntax"
- "term"
- "termination"
- "text"
- "text_raw"
- "then"
- "theorem"
- "theorems"
- "theory"
- "thm"
- "thm_deps"
- "thus"
- "thy_deps"
- "token_translation"
- "touch_child_thys"
- "touch_thy"
- "translations"
- "txt"
- "txt_raw"
- "typ"
- "typed_print_translation"
- "typedecl"
- "typedef"
- "types"
- "types_code"
- "ultimately"
- "undo"
- "undos_proof"
- "unfolding"
- "use"
- "use_thy"
- "using"
- "value"
- "welcome"
- "with"
- "{"
- "}"))
-
-(defconst isar-keywords-minor
- '("advanced"
- "and"
- "assumes"
- "attach"
- "avoids"
- "begin"
- "binder"
- "concl"
- "congs"
- "constrains"
- "contains"
- "defines"
- "distinct"
- "file"
- "fixes"
- "for"
- "freshness_context"
- "hints"
- "identifier"
- "if"
- "imports"
- "in"
- "includes"
- "induction"
- "infix"
- "infixl"
- "infixr"
- "inject"
- "invariant"
- "is"
- "local_syntax"
- "module_name"
- "monos"
- "morphisms"
- "notes"
- "obtains"
- "open"
- "otherwise"
- "output"
- "overloaded"
- "permissive"
- "sequential"
- "shows"
- "structure"
- "unchecked"
- "uses"
- "where"))
-
-(defconst isar-keywords-control
- '("ProofGeneral\\.inform_file_processed"
- "ProofGeneral\\.inform_file_retracted"
- "ProofGeneral\\.kill_proof"
- "ProofGeneral\\.process_pgip"
- "ProofGeneral\\.restart"
- "ProofGeneral\\.undo"
- "cannot_undo"
- "exit"
- "init_toplevel"
- "kill"
- "quit"
- "redo"
- "undo"
- "undos_proof"))
-
-(defconst isar-keywords-diag
- '("ML"
- "ML_command"
- "cd"
- "class_deps"
- "code_deps"
- "code_thms"
- "commit"
- "disable_pr"
- "display_drafts"
- "enable_pr"
- "export_code"
- "find_theorems"
- "full_prf"
- "header"
- "help"
- "kill_thy"
- "normal_form"
- "pr"
- "pretty_setmargin"
- "prf"
- "print_abbrevs"
- "print_antiquotations"
- "print_atp_rules"
- "print_attributes"
- "print_binds"
- "print_cases"
- "print_claset"
- "print_classes"
- "print_codesetup"
- "print_commands"
- "print_configs"
- "print_context"
- "print_drafts"
- "print_facts"
- "print_induct_rules"
- "print_interps"
- "print_locale"
- "print_locales"
- "print_methods"
- "print_noatp_rules"
- "print_orders"
- "print_rules"
- "print_simpset"
- "print_statement"
- "print_syntax"
- "print_theorems"
- "print_theory"
- "print_trans_rules"
- "prop"
- "pwd"
- "quickcheck"
- "refute"
- "remove_thy"
- "sledgehammer"
- "term"
- "thm"
- "thm_deps"
- "thy_deps"
- "touch_child_thys"
- "touch_thy"
- "typ"
- "use"
- "use_thy"
- "value"
- "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_setup"
- "abbreviation"
- "arities"
- "atom_decl"
- "axclass"
- "axiomatization"
- "axioms"
- "class"
- "classes"
- "classrel"
- "code_class"
- "code_const"
- "code_datatype"
- "code_exception"
- "code_instance"
- "code_library"
- "code_module"
- "code_modulename"
- "code_moduleprolog"
- "code_monad"
- "code_props"
- "code_reserved"
- "code_type"
- "coinductive"
- "coinductive_set"
- "constdefs"
- "consts"
- "consts_code"
- "context"
- "datatype"
- "declaration"
- "declare"
- "defaultsort"
- "defer_recdef"
- "definition"
- "defs"
- "equivariance"
- "extract"
- "extract_type"
- "finalconsts"
- "fun"
- "global"
- "hide"
- "inductive"
- "inductive_set"
- "instantiation"
- "judgment"
- "lemmas"
- "local"
- "locale"
- "method_setup"
- "no_syntax"
- "no_translations"
- "nominal_datatype"
- "nonterminals"
- "notation"
- "oracle"
- "parse_ast_translation"
- "parse_translation"
- "primrec"
- "print_ast_translation"
- "print_translation"
- "quickcheck_params"
- "realizability"
- "realizers"
- "recdef"
- "record"
- "refute_params"
- "rep_datatype"
- "setup"
- "simproc_setup"
- "syntax"
- "text"
- "text_raw"
- "theorems"
- "token_translation"
- "translations"
- "typed_print_translation"
- "typedecl"
- "types"
- "types_code"))
-
-(defconst isar-keywords-theory-script
- '("inductive_cases"))
-
-(defconst isar-keywords-theory-goal
- '("ax_specification"
- "corollary"
- "function"
- "instance"
- "instance_proof"
- "interpretation"
- "lemma"
- "nominal_inductive"
- "nominal_primrec"
- "recdef_tc"
- "specification"
- "termination"
- "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"
- "invoke"))
-
-(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"
- "show"
- "thus"))
-
-(defconst isar-keywords-proof-script
- '("apply"
- "apply_end"
- "back"
- "defer"
- "prefer"))
-
-(provide 'isar-keywords)