--- a/etc/isar-keywords-ZF.el Wed Feb 01 19:19:32 2006 +0100
+++ b/etc/isar-keywords-ZF.el Wed Feb 01 22:20:40 2006 +0100
@@ -35,13 +35,11 @@
"cd"
"chapter"
"class"
- "class_instance"
"classes"
"classrel"
"clear_undos"
"codatatype"
"code_alias"
- "code_class"
"code_generate"
"code_library"
"code_module"
@@ -216,7 +214,6 @@
"domains"
"elimination"
"file"
- "files"
"fixes"
"imports"
"in"
@@ -229,6 +226,7 @@
"is"
"monos"
"notes"
+ "obtains"
"open"
"output"
"overloaded"
@@ -342,7 +340,6 @@
"classrel"
"codatatype"
"code_alias"
- "code_class"
"code_generate"
"code_library"
"code_module"
@@ -400,8 +397,7 @@
"inductive_cases"))
(defconst isar-keywords-theory-goal
- '("class_instance"
- "corollary"
+ '("corollary"
"instance"
"interpretation"
"lemma"
--- a/etc/isar-keywords.el Wed Feb 01 19:19:32 2006 +0100
+++ b/etc/isar-keywords.el Wed Feb 01 22:20:40 2006 +0100
@@ -38,12 +38,10 @@
"cd"
"chapter"
"class"
- "class_instance"
"classes"
"classrel"
"clear_undos"
"code_alias"
- "code_class"
"code_generate"
"code_library"
"code_module"
@@ -230,7 +228,6 @@
"depending_on"
"distinct"
"file"
- "files"
"fixes"
"hide_action"
"hints"
@@ -251,6 +248,7 @@
"monos"
"morphisms"
"notes"
+ "obtains"
"open"
"output"
"outputs"
@@ -373,7 +371,6 @@
"classes"
"classrel"
"code_alias"
- "code_class"
"code_generate"
"code_library"
"code_module"
@@ -439,7 +436,6 @@
(defconst isar-keywords-theory-goal
'("ax_specification"
- "class_instance"
"corollary"
"cpodef"
"instance"