1.1 --- a/etc/isar-keywords-ZF.el	Mon Aug 20 18:07:25 2007 +0200
     1.2 +++ b/etc/isar-keywords-ZF.el	Mon Aug 20 18:07:26 2007 +0200
     1.3 @@ -37,27 +37,11 @@
     1.4      "classes"
     1.5      "classrel"
     1.6      "codatatype"
     1.7 -    "code_abstype"
     1.8 -    "code_axioms"
     1.9 -    "code_class"
    1.10 -    "code_const"
    1.11      "code_datatype"
    1.12 -    "code_deps"
    1.13 -    "code_gen"
    1.14 -    "code_instance"
    1.15 -    "code_library"
    1.16 -    "code_module"
    1.17 -    "code_modulename"
    1.18 -    "code_moduleprolog"
    1.19 -    "code_monad"
    1.20 -    "code_reserved"
    1.21 -    "code_thms"
    1.22 -    "code_type"
    1.23      "coinductive"
    1.24      "commit"
    1.25      "constdefs"
    1.26      "consts"
    1.27 -    "consts_code"
    1.28      "context"
    1.29      "corollary"
    1.30      "datatype"
    1.31 @@ -155,8 +139,6 @@
    1.32      "prop"
    1.33      "pwd"
    1.34      "qed"
    1.35 -    "quickcheck"
    1.36 -    "quickcheck_params"
    1.37      "quit"
    1.38      "realizability"
    1.39      "realizers"
    1.40 @@ -186,7 +168,6 @@
    1.41      "thus"
    1.42      "thy_deps"
    1.43      "token_translation"
    1.44 -    "touch_all_thys"
    1.45      "touch_child_thys"
    1.46      "touch_thy"
    1.47      "translations"
    1.48 @@ -196,7 +177,6 @@
    1.49      "typed_print_translation"
    1.50      "typedecl"
    1.51      "types"
    1.52 -    "types_code"
    1.53      "ultimately"
    1.54      "undo"
    1.55      "undos_proof"
    1.56 @@ -204,7 +184,6 @@
    1.57      "use"
    1.58      "use_thy"
    1.59      "using"
    1.60 -    "value"
    1.61      "welcome"
    1.62      "with"
    1.63      "{"
    1.64 @@ -221,11 +200,9 @@
    1.65      "con_defs"
    1.66      "concl"
    1.67      "constrains"
    1.68 -    "contains"
    1.69      "defines"
    1.70      "domains"
    1.71      "elimination"
    1.72 -    "file"
    1.73      "fixes"
    1.74      "for"
    1.75      "identifier"
    1.76 @@ -239,7 +216,6 @@
    1.77      "infixr"
    1.78      "intros"
    1.79      "is"
    1.80 -    "module_name"
    1.81      "monos"
    1.82      "notes"
    1.83      "obtains"
    1.84 @@ -276,9 +252,6 @@
    1.85      "ML_command"
    1.86      "cd"
    1.87      "class_deps"
    1.88 -    "code_deps"
    1.89 -    "code_gen"
    1.90 -    "code_thms"
    1.91      "commit"
    1.92      "disable_pr"
    1.93      "display_drafts"
    1.94 @@ -319,19 +292,16 @@
    1.95      "print_trans_rules"
    1.96      "prop"
    1.97      "pwd"
    1.98 -    "quickcheck"
    1.99      "remove_thy"
   1.100      "term"
   1.101      "thm"
   1.102      "thm_deps"
   1.103      "thy_deps"
   1.104 -    "touch_all_thys"
   1.105      "touch_child_thys"
   1.106      "touch_thy"
   1.107      "typ"
   1.108      "use"
   1.109      "use_thy"
   1.110 -    "value"
   1.111      "welcome"))
   1.112  
   1.113  (defconst isar-keywords-theory-begin
   1.114 @@ -360,23 +330,10 @@
   1.115      "classes"
   1.116      "classrel"
   1.117      "codatatype"
   1.118 -    "code_abstype"
   1.119 -    "code_axioms"
   1.120 -    "code_class"
   1.121 -    "code_const"
   1.122      "code_datatype"
   1.123 -    "code_instance"
   1.124 -    "code_library"
   1.125 -    "code_module"
   1.126 -    "code_modulename"
   1.127 -    "code_moduleprolog"
   1.128 -    "code_monad"
   1.129 -    "code_reserved"
   1.130 -    "code_type"
   1.131      "coinductive"
   1.132      "constdefs"
   1.133      "consts"
   1.134 -    "consts_code"
   1.135      "context"
   1.136      "datatype"
   1.137      "declaration"
   1.138 @@ -405,7 +362,6 @@
   1.139      "primrec"
   1.140      "print_ast_translation"
   1.141      "print_translation"
   1.142 -    "quickcheck_params"
   1.143      "realizability"
   1.144      "realizers"
   1.145      "rep_datatype"
   1.146 @@ -419,8 +375,7 @@
   1.147      "translations"
   1.148      "typed_print_translation"
   1.149      "typedecl"
   1.150 -    "types"
   1.151 -    "types_code"))
   1.152 +    "types"))
   1.153  
   1.154  (defconst isar-keywords-theory-script
   1.155    '("inductive_cases"))