--- 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