# HG changeset patch
# User wenzelm
# Date 1140110752 -3600
# Node ID a4b956f8b233598caab0bd2c40fc7d38cda0170d
# Parent  04b302f2902d22f94bbcad49ad71ff3a1fdadb8d
updated;

diff -r 04b302f2902d -r a4b956f8b233 etc/isar-keywords-ZF.el
--- 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"
diff -r 04b302f2902d -r a4b956f8b233 etc/isar-keywords.el
--- 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"