1.1 --- a/etc/isar-keywords-ZF.el	Fri Oct 05 23:04:17 2007 +0200
     1.2 +++ b/etc/isar-keywords-ZF.el	Sat Oct 06 16:41:22 2007 +0200
     1.3 @@ -38,10 +38,13 @@
     1.4      "classrel"
     1.5      "codatatype"
     1.6      "code_datatype"
     1.7 +    "code_library"
     1.8 +    "code_module"
     1.9      "coinductive"
    1.10      "commit"
    1.11      "constdefs"
    1.12      "consts"
    1.13 +    "consts_code"
    1.14      "context"
    1.15      "corollary"
    1.16      "datatype"
    1.17 @@ -77,6 +80,8 @@
    1.18      "inductive_cases"
    1.19      "init_toplevel"
    1.20      "instance"
    1.21 +    "instance_proof"
    1.22 +    "instantiation"
    1.23      "interpret"
    1.24      "interpretation"
    1.25      "invoke"
    1.26 @@ -139,6 +144,8 @@
    1.27      "prop"
    1.28      "pwd"
    1.29      "qed"
    1.30 +    "quickcheck"
    1.31 +    "quickcheck_params"
    1.32      "quit"
    1.33      "realizability"
    1.34      "realizers"
    1.35 @@ -177,6 +184,7 @@
    1.36      "typed_print_translation"
    1.37      "typedecl"
    1.38      "types"
    1.39 +    "types_code"
    1.40      "ultimately"
    1.41      "undo"
    1.42      "undos_proof"
    1.43 @@ -184,6 +192,7 @@
    1.44      "use"
    1.45      "use_thy"
    1.46      "using"
    1.47 +    "value"
    1.48      "welcome"
    1.49      "with"
    1.50      "{"
    1.51 @@ -200,9 +209,11 @@
    1.52      "con_defs"
    1.53      "concl"
    1.54      "constrains"
    1.55 +    "contains"
    1.56      "defines"
    1.57      "domains"
    1.58      "elimination"
    1.59 +    "file"
    1.60      "fixes"
    1.61      "for"
    1.62      "identifier"
    1.63 @@ -216,6 +227,7 @@
    1.64      "infixr"
    1.65      "intros"
    1.66      "is"
    1.67 +    "local_syntax"
    1.68      "monos"
    1.69      "notes"
    1.70      "obtains"
    1.71 @@ -292,6 +304,7 @@
    1.72      "print_trans_rules"
    1.73      "prop"
    1.74      "pwd"
    1.75 +    "quickcheck"
    1.76      "remove_thy"
    1.77      "term"
    1.78      "thm"
    1.79 @@ -302,6 +315,7 @@
    1.80      "typ"
    1.81      "use"
    1.82      "use_thy"
    1.83 +    "value"
    1.84      "welcome"))
    1.85  
    1.86  (defconst isar-keywords-theory-begin
    1.87 @@ -331,9 +345,12 @@
    1.88      "classrel"
    1.89      "codatatype"
    1.90      "code_datatype"
    1.91 +    "code_library"
    1.92 +    "code_module"
    1.93      "coinductive"
    1.94      "constdefs"
    1.95      "consts"
    1.96 +    "consts_code"
    1.97      "context"
    1.98      "datatype"
    1.99      "declaration"
   1.100 @@ -347,6 +364,7 @@
   1.101      "global"
   1.102      "hide"
   1.103      "inductive"
   1.104 +    "instantiation"
   1.105      "judgment"
   1.106      "lemmas"
   1.107      "local"
   1.108 @@ -362,6 +380,7 @@
   1.109      "primrec"
   1.110      "print_ast_translation"
   1.111      "print_translation"
   1.112 +    "quickcheck_params"
   1.113      "realizability"
   1.114      "realizers"
   1.115      "rep_datatype"
   1.116 @@ -375,7 +394,8 @@
   1.117      "translations"
   1.118      "typed_print_translation"
   1.119      "typedecl"
   1.120 -    "types"))
   1.121 +    "types"
   1.122 +    "types_code"))
   1.123  
   1.124  (defconst isar-keywords-theory-script
   1.125    '("inductive_cases"))
   1.126 @@ -383,6 +403,7 @@
   1.127  (defconst isar-keywords-theory-goal
   1.128    '("corollary"
   1.129      "instance"
   1.130 +    "instance_proof"
   1.131      "interpretation"
   1.132      "lemma"
   1.133      "theorem"))