# HG changeset patch
# User haftmann
# Date 1188207259 -7200
# Node ID c2a76e8a3d5453a6820be88afa64b41937d5a5c4
# Parent  b694324cd2be28d4e0fb00e8285e76632a40deef
updated keywords

diff -r b694324cd2be -r c2a76e8a3d54 etc/isar-keywords-HOL-Nominal.el
--- a/etc/isar-keywords-HOL-Nominal.el	Mon Aug 27 11:34:18 2007 +0200
+++ b/etc/isar-keywords-HOL-Nominal.el	Mon Aug 27 11:34:19 2007 +0200
@@ -38,8 +38,6 @@
     "class_deps"
     "classes"
     "classrel"
-    "code_abstype"
-    "code_axioms"
     "code_class"
     "code_const"
     "code_datatype"
@@ -50,6 +48,7 @@
     "code_modulename"
     "code_moduleprolog"
     "code_monad"
+    "code_props"
     "code_reserved"
     "code_thms"
     "code_type"
@@ -100,6 +99,8 @@
     "inductive_set"
     "init_toplevel"
     "instance"
+    "instance_proof"
+    "instantiation"
     "interpret"
     "interpretation"
     "invoke"
@@ -386,8 +387,6 @@
     "class"
     "classes"
     "classrel"
-    "code_abstype"
-    "code_axioms"
     "code_class"
     "code_const"
     "code_datatype"
@@ -397,6 +396,7 @@
     "code_modulename"
     "code_moduleprolog"
     "code_monad"
+    "code_props"
     "code_reserved"
     "code_type"
     "coinductive"
@@ -421,6 +421,7 @@
     "hide"
     "inductive"
     "inductive_set"
+    "instantiation"
     "judgment"
     "lemmas"
     "local"
@@ -465,6 +466,7 @@
     "corollary"
     "function"
     "instance"
+    "instance_proof"
     "interpretation"
     "lemma"
     "nominal_inductive"
diff -r b694324cd2be -r c2a76e8a3d54 etc/isar-keywords.el
--- a/etc/isar-keywords.el	Mon Aug 27 11:34:18 2007 +0200
+++ b/etc/isar-keywords.el	Mon Aug 27 11:34:19 2007 +0200
@@ -38,8 +38,6 @@
     "class_deps"
     "classes"
     "classrel"
-    "code_abstype"
-    "code_axioms"
     "code_class"
     "code_const"
     "code_datatype"
@@ -50,6 +48,7 @@
     "code_modulename"
     "code_moduleprolog"
     "code_monad"
+    "code_props"
     "code_reserved"
     "code_thms"
     "code_type"
@@ -103,6 +102,8 @@
     "inductive_set"
     "init_toplevel"
     "instance"
+    "instance_proof"
+    "instantiation"
     "interpret"
     "interpretation"
     "invoke"
@@ -401,8 +402,6 @@
     "class"
     "classes"
     "classrel"
-    "code_abstype"
-    "code_axioms"
     "code_class"
     "code_const"
     "code_datatype"
@@ -412,6 +411,7 @@
     "code_modulename"
     "code_moduleprolog"
     "code_monad"
+    "code_props"
     "code_reserved"
     "code_type"
     "coinductive"
@@ -438,6 +438,7 @@
     "hide"
     "inductive"
     "inductive_set"
+    "instantiation"
     "judgment"
     "lemmas"
     "local"
@@ -482,6 +483,7 @@
     "cpodef"
     "function"
     "instance"
+    "instance_proof"
     "interpretation"
     "lemma"
     "pcpodef"