# HG changeset patch
# User haftmann
# Date 1132659779 -3600
# Node ID 6c84210902db61638e5a28c4a7489e6ec18413eb
# Parent  9a7ffce389c310852c1aeefc9bdb180657fd8788
added code generator syntax

diff -r 9a7ffce389c3 -r 6c84210902db etc/isar-keywords-ZF.el
--- a/etc/isar-keywords-ZF.el	Tue Nov 22 10:09:11 2005 +0100
+++ b/etc/isar-keywords-ZF.el	Tue Nov 22 12:42:59 2005 +0100
@@ -37,8 +37,12 @@
     "classrel"
     "clear_undos"
     "codatatype"
+    "code_generate"
     "code_library"
     "code_module"
+    "code_syntax_const"
+    "code_syntax_tyco"
+    "codegen_class"
     "coinductive"
     "commit"
     "constdefs"
@@ -51,6 +55,7 @@
     "def"
     "defaultsort"
     "defer"
+    "defined_by"
     "defs"
     "disable_pr"
     "display_drafts"
@@ -193,13 +198,16 @@
     "begin"
     "binder"
     "case_eqns"
+    "code_alias"
     "con_defs"
     "concl"
     "constrains"
     "contains"
     "defines"
+    "depending_on"
     "domains"
     "elimination"
+    "extracting"
     "file"
     "files"
     "fixes"
@@ -323,14 +331,19 @@
     "classes"
     "classrel"
     "codatatype"
+    "code_generate"
     "code_library"
     "code_module"
+    "code_syntax_const"
+    "code_syntax_tyco"
+    "codegen_class"
     "coinductive"
     "constdefs"
     "consts"
     "consts_code"
     "datatype"
     "defaultsort"
+    "defined_by"
     "defs"
     "extract"
     "extract_type"
diff -r 9a7ffce389c3 -r 6c84210902db etc/isar-keywords.el
--- a/etc/isar-keywords.el	Tue Nov 22 10:09:11 2005 +0100
+++ b/etc/isar-keywords.el	Tue Nov 22 12:42:59 2005 +0100
@@ -39,8 +39,11 @@
     "classes"
     "classrel"
     "clear_undos"
+    "code_generate"
     "code_library"
     "code_module"
+    "code_syntax_const"
+    "code_syntax_tyco"
     "codegen_class"
     "coinductive"
     "commit"
@@ -56,6 +59,7 @@
     "defaultsort"
     "defer"
     "defer_recdef"
+    "defined_by"
     "defs"
     "disable_pr"
     "display_drafts"
@@ -208,13 +212,16 @@
     "attach"
     "begin"
     "binder"
+    "code_alias"
     "compose"
     "concl"
     "congs"
     "constrains"
     "contains"
     "defines"
+    "depending_on"
     "distinct"
+    "extracting"
     "file"
     "files"
     "fixes"
@@ -355,8 +362,11 @@
     "axioms"
     "classes"
     "classrel"
+    "code_generate"
     "code_library"
     "code_module"
+    "code_syntax_const"
+    "code_syntax_tyco"
     "codegen_class"
     "coinductive"
     "constdefs"
@@ -365,6 +375,7 @@
     "datatype"
     "defaultsort"
     "defer_recdef"
+    "defined_by"
     "defs"
     "domain"
     "extract"