Fixed legacy locale keywords (went to ZF rather than default keywords file).
--- a/etc/isar-keywords-ZF.el Sun Dec 14 15:50:21 2008 +0100
+++ b/etc/isar-keywords-ZF.el Sun Dec 14 18:45:16 2008 +0100
@@ -40,9 +40,6 @@
"chapter"
"class"
"class_deps"
- "class_interpret"
- "class_interpretation"
- "class_locale"
"classes"
"classrel"
"codatatype"
@@ -352,7 +349,6 @@
"axiomatization"
"axioms"
"class"
- "class_locale"
"classes"
"classrel"
"codatatype"
@@ -415,8 +411,7 @@
'("inductive_cases"))
(defconst isar-keywords-theory-goal
- '("class_interpretation"
- "corollary"
+ '("corollary"
"instance"
"interpretation"
"lemma"
@@ -443,8 +438,7 @@
"subsubsect"))
(defconst isar-keywords-proof-goal
- '("class_interpret"
- "have"
+ '("have"
"hence"
"interpret"
"invoke"))
--- a/etc/isar-keywords.el Sun Dec 14 15:50:21 2008 +0100
+++ b/etc/isar-keywords.el Sun Dec 14 18:45:16 2008 +0100
@@ -45,6 +45,9 @@
"chapter"
"class"
"class_deps"
+ "class_interpret"
+ "class_interpretation"
+ "class_locale"
"classes"
"classrel"
"code_abort"
@@ -418,6 +421,7 @@
"axiomatization"
"axioms"
"class"
+ "class_locale"
"classes"
"classrel"
"code_abort"
@@ -501,6 +505,7 @@
(defconst isar-keywords-theory-goal
'("ax_specification"
+ "class_interpretation"
"corollary"
"cpodef"
"function"
@@ -539,7 +544,8 @@
"subsubsect"))
(defconst isar-keywords-proof-goal
- '("have"
+ '("class_interpret"
+ "have"
"hence"
"interpret"
"invoke"))