--- a/etc/isar-keywords-ZF.el Thu Feb 16 14:59:57 2006 +0100
+++ b/etc/isar-keywords-ZF.el Thu Feb 16 18:25:52 2006 +0100
@@ -20,6 +20,7 @@
"ProofGeneral\\.restart"
"ProofGeneral\\.try_context_thy_only"
"ProofGeneral\\.undo"
+ "abbreviation"
"also"
"apply"
"apply_end"
@@ -35,6 +36,7 @@
"cd"
"chapter"
"class"
+ "class_exp"
"classes"
"classrel"
"clear_undos"
@@ -210,7 +212,6 @@
"constrains"
"contains"
"defines"
- "depending_on"
"domains"
"elimination"
"file"
@@ -331,6 +332,7 @@
(defconst isar-keywords-theory-decl
'("ML_setup"
+ "abbreviation"
"arities"
"axclass"
"axiomatization"
@@ -397,7 +399,8 @@
"inductive_cases"))
(defconst isar-keywords-theory-goal
- '("corollary"
+ '("class_exp"
+ "corollary"
"instance"
"interpretation"
"lemma"
--- a/etc/isar-keywords.el Thu Feb 16 14:59:57 2006 +0100
+++ b/etc/isar-keywords.el Thu Feb 16 18:25:52 2006 +0100
@@ -21,6 +21,7 @@
"ProofGeneral\\.restart"
"ProofGeneral\\.try_context_thy_only"
"ProofGeneral\\.undo"
+ "abbreviation"
"also"
"apply"
"apply_end"
@@ -38,6 +39,7 @@
"cd"
"chapter"
"class"
+ "class_exp"
"classes"
"classrel"
"clear_undos"
@@ -225,7 +227,6 @@
"constrains"
"contains"
"defines"
- "depending_on"
"distinct"
"file"
"fixes"
@@ -362,6 +363,7 @@
(defconst isar-keywords-theory-decl
'("ML_setup"
+ "abbreviation"
"arities"
"automaton"
"axclass"
@@ -436,6 +438,7 @@
(defconst isar-keywords-theory-goal
'("ax_specification"
+ "class_exp"
"corollary"
"cpodef"
"instance"