etc/isar-keywords.el
changeset 49074 d8af889dcbe3
parent 49020 f379cf5d71bd
child 49112 4de4635d8f93
--- a/etc/isar-keywords.el	Mon Sep 03 11:30:29 2012 +0200
+++ b/etc/isar-keywords.el	Mon Sep 03 11:54:21 2012 +0200
@@ -32,10 +32,7 @@
     "axiomatization"
     "axioms"
     "back"
-    "bnf_codata"
-    "bnf_data"
     "bnf_def"
-    "bnf_sugar"
     "boogie_end"
     "boogie_open"
     "boogie_status"
@@ -50,6 +47,7 @@
     "class_deps"
     "classes"
     "classrel"
+    "codata_raw"
     "code_abort"
     "code_class"
     "code_const"
@@ -71,6 +69,7 @@
     "context"
     "corollary"
     "cpodef"
+    "data_raw"
     "datatype"
     "declaration"
     "declare"
@@ -294,6 +293,7 @@
     "values"
     "welcome"
     "with"
+    "wrap_data"
     "write"
     "{"
     "}"))
@@ -469,14 +469,13 @@
     "attribute_setup"
     "axiomatization"
     "axioms"
-    "bnf_codata"
-    "bnf_data"
     "boogie_end"
     "boogie_open"
     "bundle"
     "class"
     "classes"
     "classrel"
+    "codata_raw"
     "code_abort"
     "code_class"
     "code_const"
@@ -492,6 +491,7 @@
     "coinductive_set"
     "consts"
     "context"
+    "data_raw"
     "datatype"
     "declaration"
     "declare"
@@ -577,7 +577,6 @@
 (defconst isar-keywords-theory-goal
   '("ax_specification"
     "bnf_def"
-    "bnf_sugar"
     "boogie_vc"
     "code_pred"
     "corollary"
@@ -605,7 +604,8 @@
     "sublocale"
     "termination"
     "theorem"
-    "typedef"))
+    "typedef"
+    "wrap_data"))
 
 (defconst isar-keywords-qed
   '("\\."