# HG changeset patch
# User wenzelm
# Date 1138828840 -3600
# Node ID 3b643f81b378a3b853c374ca0016173ce4e736b2
# Parent  6ad81e3fa4782ee71ab21fdc1aeb41190d35490e
updated;

diff -r 6ad81e3fa478 -r 3b643f81b378 etc/isar-keywords-ZF.el
--- 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"
diff -r 6ad81e3fa478 -r 3b643f81b378 etc/isar-keywords.el
--- 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"