1.1 --- a/etc/isar-keywords-ZF.el	Wed Apr 22 11:10:23 2009 +0200
     1.2 +++ b/etc/isar-keywords-ZF.el	Mon May 11 09:18:42 2009 +0200
     1.3 @@ -18,7 +18,6 @@
     1.4      "ML"
     1.5      "ML_command"
     1.6      "ML_prf"
     1.7 -    "ML_test"
     1.8      "ML_val"
     1.9      "ProofGeneral\\.inform_file_processed"
    1.10      "ProofGeneral\\.inform_file_retracted"
    1.11 @@ -46,18 +45,15 @@
    1.12      "class_deps"
    1.13      "classes"
    1.14      "classrel"
    1.15 -    "codatatype"
    1.16      "code_datatype"
    1.17      "code_library"
    1.18      "code_module"
    1.19 -    "coinductive"
    1.20      "commit"
    1.21      "constdefs"
    1.22      "consts"
    1.23      "consts_code"
    1.24      "context"
    1.25      "corollary"
    1.26 -    "datatype"
    1.27      "declaration"
    1.28      "declare"
    1.29      "def"
    1.30 @@ -87,8 +83,6 @@
    1.31      "help"
    1.32      "hence"
    1.33      "hide"
    1.34 -    "inductive"
    1.35 -    "inductive_cases"
    1.36      "init_toplevel"
    1.37      "instance"
    1.38      "instantiation"
    1.39 @@ -124,7 +118,6 @@
    1.40      "presume"
    1.41      "pretty_setmargin"
    1.42      "prf"
    1.43 -    "primrec"
    1.44      "print_abbrevs"
    1.45      "print_antiquotations"
    1.46      "print_ast_translation"
    1.47 @@ -147,7 +140,6 @@
    1.48      "print_simpset"
    1.49      "print_statement"
    1.50      "print_syntax"
    1.51 -    "print_tcset"
    1.52      "print_theorems"
    1.53      "print_theory"
    1.54      "print_trans_rules"
    1.55 @@ -162,7 +154,6 @@
    1.56      "realizability"
    1.57      "realizers"
    1.58      "remove_thy"
    1.59 -    "rep_datatype"
    1.60      "sect"
    1.61      "section"
    1.62      "setup"
    1.63 @@ -216,13 +207,9 @@
    1.64      "attach"
    1.65      "begin"
    1.66      "binder"
    1.67 -    "case_eqns"
    1.68 -    "con_defs"
    1.69      "constrains"
    1.70      "contains"
    1.71      "defines"
    1.72 -    "domains"
    1.73 -    "elimination"
    1.74      "file"
    1.75      "fixes"
    1.76      "for"
    1.77 @@ -230,23 +217,17 @@
    1.78      "if"
    1.79      "imports"
    1.80      "in"
    1.81 -    "induction"
    1.82      "infix"
    1.83      "infixl"
    1.84      "infixr"
    1.85 -    "intros"
    1.86      "is"
    1.87 -    "monos"
    1.88      "notes"
    1.89      "obtains"
    1.90      "open"
    1.91      "output"
    1.92      "overloaded"
    1.93 -    "recursor_eqns"
    1.94      "shows"
    1.95      "structure"
    1.96 -    "type_elims"
    1.97 -    "type_intros"
    1.98      "unchecked"
    1.99      "uses"
   1.100      "where"))
   1.101 @@ -314,7 +295,6 @@
   1.102      "print_simpset"
   1.103      "print_statement"
   1.104      "print_syntax"
   1.105 -    "print_tcset"
   1.106      "print_theorems"
   1.107      "print_theory"
   1.108      "print_trans_rules"
   1.109 @@ -349,7 +329,6 @@
   1.110  
   1.111  (defconst isar-keywords-theory-decl
   1.112    '("ML"
   1.113 -    "ML_test"
   1.114      "abbreviation"
   1.115      "arities"
   1.116      "attribute_setup"
   1.117 @@ -359,16 +338,13 @@
   1.118      "class"
   1.119      "classes"
   1.120      "classrel"
   1.121 -    "codatatype"
   1.122      "code_datatype"
   1.123      "code_library"
   1.124      "code_module"
   1.125 -    "coinductive"
   1.126      "constdefs"
   1.127      "consts"
   1.128      "consts_code"
   1.129      "context"
   1.130 -    "datatype"
   1.131      "declaration"
   1.132      "declare"
   1.133      "defaultsort"
   1.134 @@ -379,7 +355,6 @@
   1.135      "finalconsts"
   1.136      "global"
   1.137      "hide"
   1.138 -    "inductive"
   1.139      "instantiation"
   1.140      "judgment"
   1.141      "lemmas"
   1.142 @@ -396,13 +371,11 @@
   1.143      "overloading"
   1.144      "parse_ast_translation"
   1.145      "parse_translation"
   1.146 -    "primrec"
   1.147      "print_ast_translation"
   1.148      "print_translation"
   1.149      "quickcheck_params"
   1.150      "realizability"
   1.151      "realizers"
   1.152 -    "rep_datatype"
   1.153      "setup"
   1.154      "simproc_setup"
   1.155      "syntax"
   1.156 @@ -417,7 +390,7 @@
   1.157      "use"))
   1.158  
   1.159  (defconst isar-keywords-theory-script
   1.160 -  '("inductive_cases"))
   1.161 +  '())
   1.162  
   1.163  (defconst isar-keywords-theory-goal
   1.164    '("corollary"