etc/isar-keywords-ZF.el
changeset 15598 4ab52355bb53
parent 15596 8665d08085df
child 15624 484178635bd8
--- a/etc/isar-keywords-ZF.el	Thu Mar 10 09:11:57 2005 +0100
+++ b/etc/isar-keywords-ZF.el	Thu Mar 10 17:48:36 2005 +0100
@@ -74,6 +74,7 @@
     "init_toplevel"
     "instance"
     "instantiate"
+    "interpretation"
     "judgment"
     "kill"
     "kill_thy"
@@ -109,11 +110,11 @@
     "print_drafts"
     "print_facts"
     "print_induct_rules"
+    "print_interps"
     "print_intros"
     "print_locale"
     "print_locales"
     "print_methods"
-    "print_registrations"
     "print_rules"
     "print_simpset"
     "print_syntax"
@@ -132,7 +133,6 @@
     "realizability"
     "realizers"
     "redo"
-    "registration"
     "remove_thy"
     "rep_datatype"
     "sect"
@@ -261,11 +261,11 @@
     "print_drafts"
     "print_facts"
     "print_induct_rules"
+    "print_interps"
     "print_intros"
     "print_locale"
     "print_locales"
     "print_methods"
-    "print_registrations"
     "print_rules"
     "print_simpset"
     "print_syntax"
@@ -364,8 +364,8 @@
 (defconst isar-keywords-theory-goal
   '("corollary"
     "instance"
+    "interpretation"
     "lemma"
-    "registration"
     "theorem"))
 
 (defconst isar-keywords-qed