1.1 --- a/etc/isar-keywords-HOL-Nominal.el Mon Aug 20 18:07:25 2007 +0200
1.2 +++ b/etc/isar-keywords-HOL-Nominal.el Mon Aug 20 18:07:26 2007 +0200
1.3 @@ -44,7 +44,6 @@
1.4 "code_const"
1.5 "code_datatype"
1.6 "code_deps"
1.7 - "code_gen"
1.8 "code_instance"
1.9 "code_library"
1.10 "code_module"
1.11 @@ -78,6 +77,7 @@
1.12 "end"
1.13 "equivariance"
1.14 "exit"
1.15 + "export_code"
1.16 "extract"
1.17 "extract_type"
1.18 "finalconsts"
1.19 @@ -154,6 +154,7 @@
1.20 "print_locale"
1.21 "print_locales"
1.22 "print_methods"
1.23 + "print_noatp_rules"
1.24 "print_rules"
1.25 "print_simpset"
1.26 "print_statement"
1.27 @@ -205,7 +206,6 @@
1.28 "thus"
1.29 "thy_deps"
1.30 "token_translation"
1.31 - "touch_all_thys"
1.32 "touch_child_thys"
1.33 "touch_thy"
1.34 "translations"
1.35 @@ -300,12 +300,12 @@
1.36 "cd"
1.37 "class_deps"
1.38 "code_deps"
1.39 - "code_gen"
1.40 "code_thms"
1.41 "commit"
1.42 "disable_pr"
1.43 "display_drafts"
1.44 "enable_pr"
1.45 + "export_code"
1.46 "find_theorems"
1.47 "full_prf"
1.48 "header"
1.49 @@ -334,6 +334,7 @@
1.50 "print_locale"
1.51 "print_locales"
1.52 "print_methods"
1.53 + "print_noatp_rules"
1.54 "print_rules"
1.55 "print_simpset"
1.56 "print_statement"
1.57 @@ -351,7 +352,6 @@
1.58 "thm"
1.59 "thm_deps"
1.60 "thy_deps"
1.61 - "touch_all_thys"
1.62 "touch_child_thys"
1.63 "touch_thy"
1.64 "typ"
2.1 --- a/etc/isar-keywords-ZF.el Mon Aug 20 18:07:25 2007 +0200
2.2 +++ b/etc/isar-keywords-ZF.el Mon Aug 20 18:07:26 2007 +0200
2.3 @@ -37,27 +37,11 @@
2.4 "classes"
2.5 "classrel"
2.6 "codatatype"
2.7 - "code_abstype"
2.8 - "code_axioms"
2.9 - "code_class"
2.10 - "code_const"
2.11 "code_datatype"
2.12 - "code_deps"
2.13 - "code_gen"
2.14 - "code_instance"
2.15 - "code_library"
2.16 - "code_module"
2.17 - "code_modulename"
2.18 - "code_moduleprolog"
2.19 - "code_monad"
2.20 - "code_reserved"
2.21 - "code_thms"
2.22 - "code_type"
2.23 "coinductive"
2.24 "commit"
2.25 "constdefs"
2.26 "consts"
2.27 - "consts_code"
2.28 "context"
2.29 "corollary"
2.30 "datatype"
2.31 @@ -155,8 +139,6 @@
2.32 "prop"
2.33 "pwd"
2.34 "qed"
2.35 - "quickcheck"
2.36 - "quickcheck_params"
2.37 "quit"
2.38 "realizability"
2.39 "realizers"
2.40 @@ -186,7 +168,6 @@
2.41 "thus"
2.42 "thy_deps"
2.43 "token_translation"
2.44 - "touch_all_thys"
2.45 "touch_child_thys"
2.46 "touch_thy"
2.47 "translations"
2.48 @@ -196,7 +177,6 @@
2.49 "typed_print_translation"
2.50 "typedecl"
2.51 "types"
2.52 - "types_code"
2.53 "ultimately"
2.54 "undo"
2.55 "undos_proof"
2.56 @@ -204,7 +184,6 @@
2.57 "use"
2.58 "use_thy"
2.59 "using"
2.60 - "value"
2.61 "welcome"
2.62 "with"
2.63 "{"
2.64 @@ -221,11 +200,9 @@
2.65 "con_defs"
2.66 "concl"
2.67 "constrains"
2.68 - "contains"
2.69 "defines"
2.70 "domains"
2.71 "elimination"
2.72 - "file"
2.73 "fixes"
2.74 "for"
2.75 "identifier"
2.76 @@ -239,7 +216,6 @@
2.77 "infixr"
2.78 "intros"
2.79 "is"
2.80 - "module_name"
2.81 "monos"
2.82 "notes"
2.83 "obtains"
2.84 @@ -276,9 +252,6 @@
2.85 "ML_command"
2.86 "cd"
2.87 "class_deps"
2.88 - "code_deps"
2.89 - "code_gen"
2.90 - "code_thms"
2.91 "commit"
2.92 "disable_pr"
2.93 "display_drafts"
2.94 @@ -319,19 +292,16 @@
2.95 "print_trans_rules"
2.96 "prop"
2.97 "pwd"
2.98 - "quickcheck"
2.99 "remove_thy"
2.100 "term"
2.101 "thm"
2.102 "thm_deps"
2.103 "thy_deps"
2.104 - "touch_all_thys"
2.105 "touch_child_thys"
2.106 "touch_thy"
2.107 "typ"
2.108 "use"
2.109 "use_thy"
2.110 - "value"
2.111 "welcome"))
2.112
2.113 (defconst isar-keywords-theory-begin
2.114 @@ -360,23 +330,10 @@
2.115 "classes"
2.116 "classrel"
2.117 "codatatype"
2.118 - "code_abstype"
2.119 - "code_axioms"
2.120 - "code_class"
2.121 - "code_const"
2.122 "code_datatype"
2.123 - "code_instance"
2.124 - "code_library"
2.125 - "code_module"
2.126 - "code_modulename"
2.127 - "code_moduleprolog"
2.128 - "code_monad"
2.129 - "code_reserved"
2.130 - "code_type"
2.131 "coinductive"
2.132 "constdefs"
2.133 "consts"
2.134 - "consts_code"
2.135 "context"
2.136 "datatype"
2.137 "declaration"
2.138 @@ -405,7 +362,6 @@
2.139 "primrec"
2.140 "print_ast_translation"
2.141 "print_translation"
2.142 - "quickcheck_params"
2.143 "realizability"
2.144 "realizers"
2.145 "rep_datatype"
2.146 @@ -419,8 +375,7 @@
2.147 "translations"
2.148 "typed_print_translation"
2.149 "typedecl"
2.150 - "types"
2.151 - "types_code"))
2.152 + "types"))
2.153
2.154 (defconst isar-keywords-theory-script
2.155 '("inductive_cases"))
3.1 --- a/etc/isar-keywords.el Mon Aug 20 18:07:25 2007 +0200
3.2 +++ b/etc/isar-keywords.el Mon Aug 20 18:07:26 2007 +0200
3.3 @@ -44,7 +44,6 @@
3.4 "code_const"
3.5 "code_datatype"
3.6 "code_deps"
3.7 - "code_gen"
3.8 "code_instance"
3.9 "code_library"
3.10 "code_module"
3.11 @@ -79,6 +78,7 @@
3.12 "enable_pr"
3.13 "end"
3.14 "exit"
3.15 + "export_code"
3.16 "extract"
3.17 "extract_type"
3.18 "finalconsts"
3.19 @@ -155,6 +155,7 @@
3.20 "print_locale"
3.21 "print_locales"
3.22 "print_methods"
3.23 + "print_noatp_rules"
3.24 "print_rules"
3.25 "print_simpset"
3.26 "print_statement"
3.27 @@ -206,7 +207,6 @@
3.28 "thus"
3.29 "thy_deps"
3.30 "token_translation"
3.31 - "touch_all_thys"
3.32 "touch_child_thys"
3.33 "touch_thy"
3.34 "translations"
3.35 @@ -315,12 +315,12 @@
3.36 "cd"
3.37 "class_deps"
3.38 "code_deps"
3.39 - "code_gen"
3.40 "code_thms"
3.41 "commit"
3.42 "disable_pr"
3.43 "display_drafts"
3.44 "enable_pr"
3.45 + "export_code"
3.46 "find_theorems"
3.47 "full_prf"
3.48 "header"
3.49 @@ -349,6 +349,7 @@
3.50 "print_locale"
3.51 "print_locales"
3.52 "print_methods"
3.53 + "print_noatp_rules"
3.54 "print_rules"
3.55 "print_simpset"
3.56 "print_statement"
3.57 @@ -366,7 +367,6 @@
3.58 "thm"
3.59 "thm_deps"
3.60 "thy_deps"
3.61 - "touch_all_thys"
3.62 "touch_child_thys"
3.63 "touch_thy"
3.64 "typ"