# HG changeset patch # User berghofe # Date 1124985071 -7200 # Node ID fa9e28b23d7047ff16e32b4d90d45861a473d532 # Parent 67e9b86ed2119c1453e8dc3cc6483ad4ca1b264f Adapted to new code generator syntax. diff -r 67e9b86ed211 -r fa9e28b23d70 etc/isar-keywords-ZF.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" diff -r 67e9b86ed211 -r fa9e28b23d70 etc/isar-keywords.el --- 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"