update from Isabelle2009-2;

1 files changed, 219 insertions, 61 deletions

diff --git a/isar/isar-keywords.el b/isar/isar-keywords.el
index c7e0c7c2..07f9861a 100644
--- a/isar/isar-keywords.el
+++ b/isar/isar-keywords.el
@@ -1,52 +1,72 @@
-;; NB: this copy of isar-keywords is NOT usually the one that is loaded.
-;; It will only be used if Isabelle is not properly installed and the
-;; isatool command cannot be found.  It is needed as a fallback in this case.
-;;
-;; =================================================================
 ;;
 ;; Keyword classification tables for Isabelle/Isar.
-;; This file was generated by Isabelle/HOLCF/IOA -- DO NOT EDIT!
-;;
-;; $Id$
+;; Generated from Pure + Pure-ProofGeneral + HOL + HOLCF + IOA + HOL-Boogie + HOL-Nominal + HOL-Statespace.
+;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***
 ;;
 
 (defconst isar-keywords-major
   '("\\."
     "\\.\\."
+    "Isabelle\\.command"
+    "Isar\\.begin_document"
+    "Isar\\.define_command"
+    "Isar\\.edit_document"
+    "Isar\\.end_document"
     "ML"
     "ML_command"
-    "ML_setup"
-    "ProofGeneral\\.call_atp"
-    "ProofGeneral\\.context_thy_only"
+    "ML_prf"
+    "ML_val"
     "ProofGeneral\\.inform_file_processed"
     "ProofGeneral\\.inform_file_retracted"
     "ProofGeneral\\.kill_proof"
+    "ProofGeneral\\.pr"
     "ProofGeneral\\.process_pgip"
-    "ProofGeneral\\.redo"
     "ProofGeneral\\.restart"
-    "ProofGeneral\\.try_context_thy_only"
     "ProofGeneral\\.undo"
+    "abbreviation"
     "also"
     "apply"
     "apply_end"
     "arities"
     "assume"
+    "atom_decl"
+    "attribute_setup"
     "automaton"
     "ax_specification"
-    "axclass"
+    "axiomatization"
     "axioms"
     "back"
+    "boogie_end"
+    "boogie_open"
+    "boogie_status"
+    "boogie_vc"
     "by"
     "cannot_undo"
     "case"
     "cd"
     "chapter"
+    "class"
+    "class_deps"
     "classes"
     "classrel"
-    "clear_undos"
+    "code_abort"
+    "code_class"
+    "code_const"
+    "code_datatype"
+    "code_deps"
+    "code_include"
+    "code_instance"
     "code_library"
     "code_module"
+    "code_modulename"
+    "code_monad"
+    "code_pred"
+    "code_reflect"
+    "code_reserved"
+    "code_thms"
+    "code_type"
     "coinductive"
+    "coinductive_set"
     "commit"
     "constdefs"
     "consts"
@@ -55,38 +75,54 @@
     "corollary"
     "cpodef"
     "datatype"
+    "declaration"
     "declare"
     "def"
-    "defaultsort"
+    "default_sort"
     "defer"
     "defer_recdef"
+    "definition"
     "defs"
     "disable_pr"
     "display_drafts"
     "domain"
+    "domain_isomorphism"
     "done"
     "enable_pr"
     "end"
+    "equivariance"
+    "example_proof"
     "exit"
+    "export_code"
     "extract"
     "extract_type"
     "finalconsts"
     "finally"
+    "find_consts"
     "find_theorems"
     "fix"
     "fixpat"
     "fixrec"
     "from"
     "full_prf"
+    "fun"
+    "function"
     "global"
+    "guess"
     "have"
     "header"
+    "help"
     "hence"
-    "hide"
+    "hide_class"
+    "hide_const"
+    "hide_fact"
+    "hide_type"
     "inductive"
     "inductive_cases"
+    "inductive_set"
     "init_toplevel"
     "instance"
+    "instantiation"
     "interpret"
     "interpretation"
     "judgment"
@@ -95,17 +131,32 @@
     "lemma"
     "lemmas"
     "let"
+    "linear_undo"
     "local"
+    "local_setup"
     "locale"
     "method_setup"
     "moreover"
+    "new_domain"
     "next"
+    "nitpick"
+    "nitpick_params"
+    "no_notation"
     "no_syntax"
+    "no_translations"
+    "no_type_notation"
+    "nominal_datatype"
+    "nominal_inductive"
+    "nominal_inductive2"
+    "nominal_primrec"
     "nonterminals"
+    "normal_form"
+    "notation"
     "note"
     "obtain"
     "oops"
     "oracle"
+    "overloading"
     "parse_ast_translation"
     "parse_translation"
     "pcpodef"
@@ -115,13 +166,18 @@
     "pretty_setmargin"
     "prf"
     "primrec"
+    "print_abbrevs"
     "print_antiquotations"
     "print_ast_translation"
     "print_attributes"
     "print_binds"
     "print_cases"
     "print_claset"
+    "print_classes"
+    "print_codeproc"
+    "print_codesetup"
     "print_commands"
+    "print_configs"
     "print_context"
     "print_drafts"
     "print_facts"
@@ -130,8 +186,13 @@
     "print_locale"
     "print_locales"
     "print_methods"
+    "print_orders"
+    "print_quotconsts"
+    "print_quotients"
+    "print_quotmaps"
     "print_rules"
     "print_simpset"
+    "print_statement"
     "print_syntax"
     "print_theorems"
     "print_theory"
@@ -144,28 +205,41 @@
     "quickcheck"
     "quickcheck_params"
     "quit"
+    "quotient_definition"
+    "quotient_type"
     "realizability"
     "realizers"
     "recdef"
     "recdef_tc"
     "record"
-    "redo"
     "refute"
     "refute_params"
     "remove_thy"
     "rep_datatype"
+    "repdef"
+    "schematic_corollary"
+    "schematic_lemma"
+    "schematic_theorem"
     "sect"
     "section"
     "setup"
     "show"
+    "simproc_setup"
+    "sledgehammer"
+    "sledgehammer_params"
+    "smt_status"
     "sorry"
     "specification"
+    "statespace"
+    "subclass"
+    "sublocale"
     "subsect"
     "subsection"
     "subsubsect"
     "subsubsection"
     "syntax"
     "term"
+    "termination"
     "text"
     "text_raw"
     "then"
@@ -175,14 +249,13 @@
     "thm"
     "thm_deps"
     "thus"
-    "token_translation"
-    "touch_all_thys"
-    "touch_child_thys"
+    "thy_deps"
     "touch_thy"
     "translations"
     "txt"
     "txt_raw"
     "typ"
+    "type_notation"
     "typed_print_translation"
     "typedecl"
     "typedef"
@@ -191,15 +264,16 @@
     "ultimately"
     "undo"
     "undos_proof"
-    "update_thy"
-    "update_thy_only"
+    "unfolding"
+    "unused_thms"
     "use"
     "use_thy"
-    "use_thy_only"
     "using"
     "value"
+    "values"
     "welcome"
     "with"
+    "write"
     "{"
     "}"))
 
@@ -209,42 +283,44 @@
     "and"
     "assumes"
     "attach"
+    "avoids"
     "begin"
     "binder"
     "compose"
-    "concl"
     "congs"
     "constrains"
     "contains"
+    "datatypes"
     "defines"
-    "distinct"
     "file"
-    "files"
     "fixes"
+    "for"
+    "functions"
     "hide_action"
     "hints"
+    "identifier"
+    "if"
     "imports"
     "in"
-    "includes"
-    "induction"
     "infix"
     "infixl"
     "infixr"
     "initially"
-    "inject"
     "inputs"
     "internals"
-    "intros"
     "is"
     "lazy"
+    "module_name"
     "monos"
     "morphisms"
     "notes"
+    "obtains"
     "open"
     "output"
     "outputs"
     "overloaded"
     "permissive"
+    "pervasive"
     "post"
     "pre"
     "rename"
@@ -256,51 +332,67 @@
     "to"
     "transitions"
     "transrel"
+    "unchecked"
     "uses"
     "where"))
 
 (defconst isar-keywords-control
-  '("ProofGeneral\\.context_thy_only"
+  '("Isabelle\\.command"
+    "Isar\\.begin_document"
+    "Isar\\.define_command"
+    "Isar\\.edit_document"
+    "Isar\\.end_document"
     "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"
+    "linear_undo"
     "quit"
-    "redo"
     "undo"
     "undos_proof"))
 
 (defconst isar-keywords-diag
-  '("ML"
-    "ML_command"
-    "ProofGeneral\\.call_atp"
+  '("ML_command"
+    "ML_val"
+    "ProofGeneral\\.pr"
+    "boogie_status"
     "cd"
+    "class_deps"
+    "code_deps"
+    "code_thms"
     "commit"
     "disable_pr"
     "display_drafts"
     "enable_pr"
+    "export_code"
+    "find_consts"
     "find_theorems"
     "full_prf"
     "header"
+    "help"
     "kill_thy"
+    "nitpick"
+    "normal_form"
     "pr"
     "pretty_setmargin"
     "prf"
+    "print_abbrevs"
     "print_antiquotations"
     "print_attributes"
     "print_binds"
     "print_cases"
     "print_claset"
+    "print_classes"
+    "print_codeproc"
+    "print_codesetup"
     "print_commands"
+    "print_configs"
     "print_context"
     "print_drafts"
     "print_facts"
@@ -309,8 +401,13 @@
     "print_locale"
     "print_locales"
     "print_methods"
+    "print_orders"
+    "print_quotconsts"
+    "print_quotients"
+    "print_quotmaps"
     "print_rules"
     "print_simpset"
+    "print_statement"
     "print_syntax"
     "print_theorems"
     "print_theory"
@@ -320,26 +417,25 @@
     "quickcheck"
     "refute"
     "remove_thy"
+    "sledgehammer"
+    "smt_status"
     "term"
     "thm"
     "thm_deps"
-    "touch_all_thys"
-    "touch_child_thys"
+    "thy_deps"
     "touch_thy"
     "typ"
-    "update_thy"
-    "update_thy_only"
-    "use"
+    "unused_thms"
     "use_thy"
-    "use_thy_only"
     "value"
+    "values"
     "welcome"))
 
 (defconst isar-keywords-theory-begin
   '("theory"))
 
 (defconst isar-keywords-theory-switch
-  '("context"))
+  '())
 
 (defconst isar-keywords-theory-end
   '("end"))
@@ -351,78 +447,136 @@
     "subsubsection"))
 
 (defconst isar-keywords-theory-decl
-  '("ML_setup"
+  '("ML"
+    "abbreviation"
     "arities"
+    "atom_decl"
+    "attribute_setup"
     "automaton"
-    "axclass"
+    "axiomatization"
     "axioms"
+    "boogie_end"
+    "boogie_open"
+    "class"
     "classes"
     "classrel"
+    "code_abort"
+    "code_class"
+    "code_const"
+    "code_datatype"
+    "code_include"
+    "code_instance"
     "code_library"
     "code_module"
+    "code_modulename"
+    "code_monad"
+    "code_reflect"
+    "code_reserved"
+    "code_type"
     "coinductive"
+    "coinductive_set"
     "constdefs"
     "consts"
     "consts_code"
+    "context"
     "datatype"
-    "defaultsort"
+    "declaration"
+    "declare"
+    "default_sort"
     "defer_recdef"
+    "definition"
     "defs"
     "domain"
+    "domain_isomorphism"
+    "equivariance"
     "extract"
     "extract_type"
     "finalconsts"
     "fixpat"
     "fixrec"
+    "fun"
     "global"
-    "hide"
+    "hide_class"
+    "hide_const"
+    "hide_fact"
+    "hide_type"
     "inductive"
+    "inductive_set"
+    "instantiation"
     "judgment"
     "lemmas"
     "local"
+    "local_setup"
     "locale"
     "method_setup"
+    "new_domain"
+    "nitpick_params"
+    "no_notation"
     "no_syntax"
+    "no_translations"
+    "no_type_notation"
+    "nominal_datatype"
     "nonterminals"
+    "notation"
     "oracle"
+    "overloading"
     "parse_ast_translation"
     "parse_translation"
     "primrec"
     "print_ast_translation"
     "print_translation"
     "quickcheck_params"
+    "quotient_definition"
     "realizability"
     "realizers"
     "recdef"
     "record"
     "refute_params"
-    "rep_datatype"
+    "repdef"
     "setup"
+    "simproc_setup"
+    "sledgehammer_params"
+    "statespace"
     "syntax"
     "text"
     "text_raw"
     "theorems"
-    "token_translation"
     "translations"
+    "type_notation"
     "typed_print_translation"
     "typedecl"
     "types"
-    "types_code"))
+    "types_code"
+    "use"))
 
 (defconst isar-keywords-theory-script
-  '("declare"
-    "inductive_cases"))
+  '("inductive_cases"))
 
 (defconst isar-keywords-theory-goal
   '("ax_specification"
+    "boogie_vc"
+    "code_pred"
     "corollary"
     "cpodef"
+    "example_proof"
+    "function"
     "instance"
     "interpretation"
     "lemma"
+    "nominal_inductive"
+    "nominal_inductive2"
+    "nominal_primrec"
     "pcpodef"
+    "quotient_type"
     "recdef_tc"
+    "rep_datatype"
+    "schematic_corollary"
+    "schematic_lemma"
+    "schematic_theorem"
     "specification"
+    "subclass"
+    "sublocale"
+    "termination"
     "theorem"
     "typedef"))
 
@@ -447,9 +601,7 @@
 (defconst isar-keywords-proof-goal
   '("have"
     "hence"
-    "interpret"
-    "show"
-    "thus"))
+    "interpret"))
 
 (defconst isar-keywords-proof-block
   '("next"
@@ -469,13 +621,16 @@
     "with"))
 
 (defconst isar-keywords-proof-decl
-  '("also"
+  '("ML_prf"
+    "also"
     "let"
     "moreover"
     "note"
     "txt"
     "txt_raw"
-    "using"))
+    "unfolding"
+    "using"
+    "write"))
 
 (defconst isar-keywords-proof-asm
   '("assume"
@@ -485,7 +640,10 @@
     "presume"))
 
 (defconst isar-keywords-proof-asm-goal
-  '("obtain"))
+  '("guess"
+    "obtain"
+    "show"
+    "thus"))
 
 (defconst isar-keywords-proof-script
   '("apply"