1.1 --- a/etc/isar-keywords.el	Wed Apr 22 11:10:23 2009 +0200
     1.2 +++ b/etc/isar-keywords.el	Mon May 11 09:18:42 2009 +0200
     1.3 @@ -1,6 +1,6 @@
     1.4  ;;
     1.5  ;; Keyword classification tables for Isabelle/Isar.
     1.6 -;; Generated from Pure + Pure-ProofGeneral + HOL + HOLCF + IOA + HOL-Nominal + HOL-Statespace.
     1.7 +;; Generated from Pure + Pure-ProofGeneral + HOL + HOLCF + IOA + HOL-Nominal + HOL-Statespace + HOL-ex.
     1.8  ;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***
     1.9  ;;
    1.10  
    1.11 @@ -18,7 +18,6 @@
    1.12      "ML"
    1.13      "ML_command"
    1.14      "ML_prf"
    1.15 -    "ML_test"
    1.16      "ML_val"
    1.17      "ProofGeneral\\.inform_file_processed"
    1.18      "ProofGeneral\\.inform_file_retracted"
    1.19 @@ -37,7 +36,6 @@
    1.20      "atp_kill"
    1.21      "atp_messages"
    1.22      "attribute_setup"
    1.23 -    "automaton"
    1.24      "ax_specification"
    1.25      "axclass"
    1.26      "axiomatization"
    1.27 @@ -63,6 +61,7 @@
    1.28      "code_module"
    1.29      "code_modulename"
    1.30      "code_monad"
    1.31 +    "code_pred"
    1.32      "code_reserved"
    1.33      "code_thms"
    1.34      "code_type"
    1.35 @@ -74,7 +73,6 @@
    1.36      "consts_code"
    1.37      "context"
    1.38      "corollary"
    1.39 -    "cpodef"
    1.40      "datatype"
    1.41      "declaration"
    1.42      "declare"
    1.43 @@ -86,7 +84,6 @@
    1.44      "defs"
    1.45      "disable_pr"
    1.46      "display_drafts"
    1.47 -    "domain"
    1.48      "done"
    1.49      "enable_pr"
    1.50      "end"
    1.51 @@ -100,8 +97,6 @@
    1.52      "find_consts"
    1.53      "find_theorems"
    1.54      "fix"
    1.55 -    "fixpat"
    1.56 -    "fixrec"
    1.57      "from"
    1.58      "full_prf"
    1.59      "fun"
    1.60 @@ -151,7 +146,6 @@
    1.61      "overloading"
    1.62      "parse_ast_translation"
    1.63      "parse_translation"
    1.64 -    "pcpodef"
    1.65      "pr"
    1.66      "prefer"
    1.67      "presume"
    1.68 @@ -255,15 +249,13 @@
    1.69      "}"))
    1.70  
    1.71  (defconst isar-keywords-minor
    1.72 -  '("actions"
    1.73 -    "advanced"
    1.74 +  '("advanced"
    1.75      "and"
    1.76      "assumes"
    1.77      "attach"
    1.78      "avoids"
    1.79      "begin"
    1.80      "binder"
    1.81 -    "compose"
    1.82      "congs"
    1.83      "constrains"
    1.84      "contains"
    1.85 @@ -271,7 +263,6 @@
    1.86      "file"
    1.87      "fixes"
    1.88      "for"
    1.89 -    "hide_action"
    1.90      "hints"
    1.91      "identifier"
    1.92      "if"
    1.93 @@ -280,11 +271,7 @@
    1.94      "infix"
    1.95      "infixl"
    1.96      "infixr"
    1.97 -    "initially"
    1.98 -    "inputs"
    1.99 -    "internals"
   1.100      "is"
   1.101 -    "lazy"
   1.102      "module_name"
   1.103      "monos"
   1.104      "morphisms"
   1.105 @@ -292,20 +279,10 @@
   1.106      "obtains"
   1.107      "open"
   1.108      "output"
   1.109 -    "outputs"
   1.110      "overloaded"
   1.111      "permissive"
   1.112 -    "post"
   1.113 -    "pre"
   1.114 -    "rename"
   1.115 -    "restrict"
   1.116      "shows"
   1.117 -    "signature"
   1.118 -    "states"
   1.119      "structure"
   1.120 -    "to"
   1.121 -    "transitions"
   1.122 -    "transrel"
   1.123      "unchecked"
   1.124      "uses"
   1.125      "where"))
   1.126 @@ -419,12 +396,10 @@
   1.127  
   1.128  (defconst isar-keywords-theory-decl
   1.129    '("ML"
   1.130 -    "ML_test"
   1.131      "abbreviation"
   1.132      "arities"
   1.133      "atom_decl"
   1.134      "attribute_setup"
   1.135 -    "automaton"
   1.136      "axclass"
   1.137      "axiomatization"
   1.138      "axioms"
   1.139 @@ -456,13 +431,10 @@
   1.140      "defer_recdef"
   1.141      "definition"
   1.142      "defs"
   1.143 -    "domain"
   1.144      "equivariance"
   1.145      "extract"
   1.146      "extract_type"
   1.147      "finalconsts"
   1.148 -    "fixpat"
   1.149 -    "fixrec"
   1.150      "fun"
   1.151      "global"
   1.152      "hide"
   1.153 @@ -513,8 +485,8 @@
   1.154  
   1.155  (defconst isar-keywords-theory-goal
   1.156    '("ax_specification"
   1.157 +    "code_pred"
   1.158      "corollary"
   1.159 -    "cpodef"
   1.160      "function"
   1.161      "instance"
   1.162      "interpretation"
   1.163 @@ -522,7 +494,6 @@
   1.164      "nominal_inductive"
   1.165      "nominal_inductive2"
   1.166      "nominal_primrec"
   1.167 -    "pcpodef"
   1.168      "recdef_tc"
   1.169      "rep_datatype"
   1.170      "specification"