--- a/etc/isar-keywords-ZF.el Sun Apr 11 16:51:36 2010 +0200
+++ b/etc/isar-keywords-ZF.el Sun Apr 11 17:40:43 2010 +0200
@@ -43,7 +43,6 @@
"classes"
"classrel"
"codatatype"
- "code_abstype"
"code_datatype"
"code_library"
"code_module"
@@ -416,8 +415,7 @@
'("inductive_cases"))
(defconst isar-keywords-theory-goal
- '("code_abstype"
- "corollary"
+ '("corollary"
"instance"
"interpretation"
"lemma"
--- a/etc/isar-keywords.el Sun Apr 11 16:51:36 2010 +0200
+++ b/etc/isar-keywords.el Sun Apr 11 17:40:43 2010 +0200
@@ -54,7 +54,6 @@
"classes"
"classrel"
"code_abort"
- "code_abstype"
"code_class"
"code_const"
"code_datatype"
@@ -224,6 +223,7 @@
"show"
"simproc_setup"
"sledgehammer"
+ "sledgehammer_params"
"smt_status"
"sorry"
"specification"
@@ -530,6 +530,7 @@
"repdef"
"setup"
"simproc_setup"
+ "sledgehammer_params"
"statespace"
"syntax"
"text"
@@ -549,7 +550,6 @@
(defconst isar-keywords-theory-goal
'("ax_specification"
"boogie_vc"
- "code_abstype"
"code_pred"
"corollary"
"cpodef"