--- 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"