Adapted to new code generator syntax.
authorberghofe
Thu, 25 Aug 2005 17:51:11 +0200
changeset 17147 fa9e28b23d70
parent 17146 67e9b86ed211
child 17148 858cab621db2
Adapted to new code generator syntax.
etc/isar-keywords-ZF.el
etc/isar-keywords.el
--- a/etc/isar-keywords-ZF.el	Thu Aug 25 16:17:40 2005 +0200
+++ b/etc/isar-keywords-ZF.el	Thu Aug 25 17:51:11 2005 +0200
@@ -37,6 +37,8 @@
     "classrel"
     "clear_undos"
     "codatatype"
+    "code_library"
+    "code_module"
     "coinductive"
     "commit"
     "constdefs"
@@ -63,7 +65,6 @@
     "fix"
     "from"
     "full_prf"
-    "generate_code"
     "global"
     "have"
     "header"
@@ -186,15 +187,18 @@
   '("advanced"
     "and"
     "assumes"
+    "attach"
     "begin"
     "binder"
     "case_eqns"
     "con_defs"
     "concl"
     "constrains"
+    "contains"
     "defines"
     "domains"
     "elimination"
+    "file"
     "files"
     "fixes"
     "imports"
@@ -316,6 +320,8 @@
     "classes"
     "classrel"
     "codatatype"
+    "code_library"
+    "code_module"
     "coinductive"
     "constdefs"
     "consts"
@@ -326,7 +332,6 @@
     "extract"
     "extract_type"
     "finalconsts"
-    "generate_code"
     "global"
     "hide"
     "inductive"
--- a/etc/isar-keywords.el	Thu Aug 25 16:17:40 2005 +0200
+++ b/etc/isar-keywords.el	Thu Aug 25 17:51:11 2005 +0200
@@ -39,6 +39,8 @@
     "classes"
     "classrel"
     "clear_undos"
+    "code_library"
+    "code_module"
     "coinductive"
     "commit"
     "constdefs"
@@ -70,7 +72,6 @@
     "fixrec"
     "from"
     "full_prf"
-    "generate_code"
     "global"
     "have"
     "header"
@@ -208,8 +209,10 @@
     "concl"
     "congs"
     "constrains"
+    "contains"
     "defines"
     "distinct"
+    "file"
     "files"
     "fixes"
     "hide_action"
@@ -348,6 +351,8 @@
     "axioms"
     "classes"
     "classrel"
+    "code_library"
+    "code_module"
     "coinductive"
     "constdefs"
     "consts"
@@ -362,7 +367,6 @@
     "finalconsts"
     "fixpat"
     "fixrec"
-    "generate_code"
     "global"
     "hide"
     "inductive"