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