--- a/etc/isar-keywords.el Sat Oct 13 21:45:23 2001 +0200
+++ b/etc/isar-keywords.el Sat Oct 13 21:46:53 2001 +0200
@@ -1,6 +1,6 @@
;;
;; Keyword classification tables for Isabelle/Isar.
-;; This file was generated by Isabelle/HOLCF/IOA -- DO NOT EDIT!
+;; This file was generated by Isabelle/HOL -- DO NOT EDIT!
;;
;; $Id$
;;
@@ -23,7 +23,6 @@
"apply_end"
"arities"
"assume"
- "automaton"
"axclass"
"axioms"
"back"
@@ -41,6 +40,7 @@
"consts"
"consts_code"
"context"
+ "corollary"
"datatype"
"declare"
"def"
@@ -166,43 +166,27 @@
"}"))
(defconst isar-keywords-minor
- '("actions"
- "and"
+ '("and"
"binder"
- "compose"
"con_defs"
"concl"
"congs"
"distinct"
"files"
- "hide_action"
"hints"
"in"
"induction"
"infix"
"infixl"
"infixr"
- "initially"
"inject"
- "inputs"
- "internals"
"intros"
"is"
"monos"
+ "morphisms"
"output"
- "outputs"
"overloaded"
"permissive"
- "post"
- "pre"
- "rename"
- "restrict"
- "signature"
- "states"
- "to"
- "transitions"
- "transrel"
- "using"
"where"))
(defconst isar-keywords-control
@@ -287,7 +271,6 @@
(defconst isar-keywords-theory-decl
'("ML_setup"
"arities"
- "automaton"
"axclass"
"axioms"
"classes"
@@ -335,7 +318,8 @@
"inductive_cases"))
(defconst isar-keywords-theory-goal
- '("instance"
+ '("corollary"
+ "instance"
"lemma"
"recdef_tc"
"theorem"