# HG changeset patch
# User haftmann
# Date 1271000443 -7200
# Node ID e49fd7b1d932ea154fe828194555f9045070c24b
# Parent  853c777f29074c62ca7a7a5d4def25e6c48fff0b
updated keywords

diff -r 853c777f2907 -r e49fd7b1d932 etc/isar-keywords-ZF.el
--- 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"
diff -r 853c777f2907 -r e49fd7b1d932 etc/isar-keywords.el
--- 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"