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