etc/isar-keywords.el
changeset 31107 657386d94f14
parent 31106 9a1178204dc0
child 31108 0ce5f53fc65d
--- a/etc/isar-keywords.el	Mon May 11 09:18:42 2009 +0200
+++ b/etc/isar-keywords.el	Mon May 11 09:39:53 2009 +0200
@@ -1,6 +1,6 @@
 ;;
 ;; Keyword classification tables for Isabelle/Isar.
-;; Generated from Pure + Pure-ProofGeneral + HOL + HOLCF + IOA + HOL-Nominal + HOL-Statespace + HOL-ex.
+;; Generated from Pure + Pure-ProofGeneral + HOL + HOLCF + IOA + HOL-Nominal + HOL-Statespace.
 ;; *** DO NOT EDIT *** DO NOT EDIT *** DO NOT EDIT ***
 ;;
 
@@ -36,6 +36,7 @@
     "atp_kill"
     "atp_messages"
     "attribute_setup"
+    "automaton"
     "ax_specification"
     "axclass"
     "axiomatization"
@@ -73,6 +74,7 @@
     "consts_code"
     "context"
     "corollary"
+    "cpodef"
     "datatype"
     "declaration"
     "declare"
@@ -84,6 +86,7 @@
     "defs"
     "disable_pr"
     "display_drafts"
+    "domain"
     "done"
     "enable_pr"
     "end"
@@ -97,6 +100,8 @@
     "find_consts"
     "find_theorems"
     "fix"
+    "fixpat"
+    "fixrec"
     "from"
     "full_prf"
     "fun"
@@ -146,6 +151,7 @@
     "overloading"
     "parse_ast_translation"
     "parse_translation"
+    "pcpodef"
     "pr"
     "prefer"
     "presume"
@@ -249,13 +255,15 @@
     "}"))
 
 (defconst isar-keywords-minor
-  '("advanced"
+  '("actions"
+    "advanced"
     "and"
     "assumes"
     "attach"
     "avoids"
     "begin"
     "binder"
+    "compose"
     "congs"
     "constrains"
     "contains"
@@ -263,6 +271,7 @@
     "file"
     "fixes"
     "for"
+    "hide_action"
     "hints"
     "identifier"
     "if"
@@ -271,7 +280,11 @@
     "infix"
     "infixl"
     "infixr"
+    "initially"
+    "inputs"
+    "internals"
     "is"
+    "lazy"
     "module_name"
     "monos"
     "morphisms"
@@ -279,10 +292,20 @@
     "obtains"
     "open"
     "output"
+    "outputs"
     "overloaded"
     "permissive"
+    "post"
+    "pre"
+    "rename"
+    "restrict"
     "shows"
+    "signature"
+    "states"
     "structure"
+    "to"
+    "transitions"
+    "transrel"
     "unchecked"
     "uses"
     "where"))
@@ -400,6 +423,7 @@
     "arities"
     "atom_decl"
     "attribute_setup"
+    "automaton"
     "axclass"
     "axiomatization"
     "axioms"
@@ -431,10 +455,13 @@
     "defer_recdef"
     "definition"
     "defs"
+    "domain"
     "equivariance"
     "extract"
     "extract_type"
     "finalconsts"
+    "fixpat"
+    "fixrec"
     "fun"
     "global"
     "hide"
@@ -487,6 +514,7 @@
   '("ax_specification"
     "code_pred"
     "corollary"
+    "cpodef"
     "function"
     "instance"
     "interpretation"
@@ -494,6 +522,7 @@
     "nominal_inductive"
     "nominal_inductive2"
     "nominal_primrec"
+    "pcpodef"
     "recdef_tc"
     "rep_datatype"
     "specification"