--- a/etc/isar-keywords-HOL-Nominal.el Mon Aug 20 18:07:25 2007 +0200
+++ b/etc/isar-keywords-HOL-Nominal.el Mon Aug 20 18:07:26 2007 +0200
@@ -44,7 +44,6 @@
"code_const"
"code_datatype"
"code_deps"
- "code_gen"
"code_instance"
"code_library"
"code_module"
@@ -78,6 +77,7 @@
"end"
"equivariance"
"exit"
+ "export_code"
"extract"
"extract_type"
"finalconsts"
@@ -154,6 +154,7 @@
"print_locale"
"print_locales"
"print_methods"
+ "print_noatp_rules"
"print_rules"
"print_simpset"
"print_statement"
@@ -205,7 +206,6 @@
"thus"
"thy_deps"
"token_translation"
- "touch_all_thys"
"touch_child_thys"
"touch_thy"
"translations"
@@ -300,12 +300,12 @@
"cd"
"class_deps"
"code_deps"
- "code_gen"
"code_thms"
"commit"
"disable_pr"
"display_drafts"
"enable_pr"
+ "export_code"
"find_theorems"
"full_prf"
"header"
@@ -334,6 +334,7 @@
"print_locale"
"print_locales"
"print_methods"
+ "print_noatp_rules"
"print_rules"
"print_simpset"
"print_statement"
@@ -351,7 +352,6 @@
"thm"
"thm_deps"
"thy_deps"
- "touch_all_thys"
"touch_child_thys"
"touch_thy"
"typ"
--- a/etc/isar-keywords-ZF.el Mon Aug 20 18:07:25 2007 +0200
+++ b/etc/isar-keywords-ZF.el Mon Aug 20 18:07:26 2007 +0200
@@ -37,27 +37,11 @@
"classes"
"classrel"
"codatatype"
- "code_abstype"
- "code_axioms"
- "code_class"
- "code_const"
"code_datatype"
- "code_deps"
- "code_gen"
- "code_instance"
- "code_library"
- "code_module"
- "code_modulename"
- "code_moduleprolog"
- "code_monad"
- "code_reserved"
- "code_thms"
- "code_type"
"coinductive"
"commit"
"constdefs"
"consts"
- "consts_code"
"context"
"corollary"
"datatype"
@@ -155,8 +139,6 @@
"prop"
"pwd"
"qed"
- "quickcheck"
- "quickcheck_params"
"quit"
"realizability"
"realizers"
@@ -186,7 +168,6 @@
"thus"
"thy_deps"
"token_translation"
- "touch_all_thys"
"touch_child_thys"
"touch_thy"
"translations"
@@ -196,7 +177,6 @@
"typed_print_translation"
"typedecl"
"types"
- "types_code"
"ultimately"
"undo"
"undos_proof"
@@ -204,7 +184,6 @@
"use"
"use_thy"
"using"
- "value"
"welcome"
"with"
"{"
@@ -221,11 +200,9 @@
"con_defs"
"concl"
"constrains"
- "contains"
"defines"
"domains"
"elimination"
- "file"
"fixes"
"for"
"identifier"
@@ -239,7 +216,6 @@
"infixr"
"intros"
"is"
- "module_name"
"monos"
"notes"
"obtains"
@@ -276,9 +252,6 @@
"ML_command"
"cd"
"class_deps"
- "code_deps"
- "code_gen"
- "code_thms"
"commit"
"disable_pr"
"display_drafts"
@@ -319,19 +292,16 @@
"print_trans_rules"
"prop"
"pwd"
- "quickcheck"
"remove_thy"
"term"
"thm"
"thm_deps"
"thy_deps"
- "touch_all_thys"
"touch_child_thys"
"touch_thy"
"typ"
"use"
"use_thy"
- "value"
"welcome"))
(defconst isar-keywords-theory-begin
@@ -360,23 +330,10 @@
"classes"
"classrel"
"codatatype"
- "code_abstype"
- "code_axioms"
- "code_class"
- "code_const"
"code_datatype"
- "code_instance"
- "code_library"
- "code_module"
- "code_modulename"
- "code_moduleprolog"
- "code_monad"
- "code_reserved"
- "code_type"
"coinductive"
"constdefs"
"consts"
- "consts_code"
"context"
"datatype"
"declaration"
@@ -405,7 +362,6 @@
"primrec"
"print_ast_translation"
"print_translation"
- "quickcheck_params"
"realizability"
"realizers"
"rep_datatype"
@@ -419,8 +375,7 @@
"translations"
"typed_print_translation"
"typedecl"
- "types"
- "types_code"))
+ "types"))
(defconst isar-keywords-theory-script
'("inductive_cases"))
--- a/etc/isar-keywords.el Mon Aug 20 18:07:25 2007 +0200
+++ b/etc/isar-keywords.el Mon Aug 20 18:07:26 2007 +0200
@@ -44,7 +44,6 @@
"code_const"
"code_datatype"
"code_deps"
- "code_gen"
"code_instance"
"code_library"
"code_module"
@@ -79,6 +78,7 @@
"enable_pr"
"end"
"exit"
+ "export_code"
"extract"
"extract_type"
"finalconsts"
@@ -155,6 +155,7 @@
"print_locale"
"print_locales"
"print_methods"
+ "print_noatp_rules"
"print_rules"
"print_simpset"
"print_statement"
@@ -206,7 +207,6 @@
"thus"
"thy_deps"
"token_translation"
- "touch_all_thys"
"touch_child_thys"
"touch_thy"
"translations"
@@ -315,12 +315,12 @@
"cd"
"class_deps"
"code_deps"
- "code_gen"
"code_thms"
"commit"
"disable_pr"
"display_drafts"
"enable_pr"
+ "export_code"
"find_theorems"
"full_prf"
"header"
@@ -349,6 +349,7 @@
"print_locale"
"print_locales"
"print_methods"
+ "print_noatp_rules"
"print_rules"
"print_simpset"
"print_statement"
@@ -366,7 +367,6 @@
"thm"
"thm_deps"
"thy_deps"
- "touch_all_thys"
"touch_child_thys"
"touch_thy"
"typ"