1.1 --- a/etc/isar-keywords-HOL-Nominal.el	Fri Oct 05 23:04:17 2007 +0200
     1.2 +++ b/etc/isar-keywords-HOL-Nominal.el	Sat Oct 06 16:41:22 2007 +0200
     1.3 @@ -42,6 +42,7 @@
     1.4      "code_const"
     1.5      "code_datatype"
     1.6      "code_deps"
     1.7 +    "code_exception"
     1.8      "code_instance"
     1.9      "code_library"
    1.10      "code_module"
    1.11 @@ -263,6 +264,7 @@
    1.12      "inject"
    1.13      "invariant"
    1.14      "is"
    1.15 +    "local_syntax"
    1.16      "module_name"
    1.17      "monos"
    1.18      "morphisms"
    1.19 @@ -392,6 +394,7 @@
    1.20      "code_class"
    1.21      "code_const"
    1.22      "code_datatype"
    1.23 +    "code_exception"
    1.24      "code_instance"
    1.25      "code_library"
    1.26      "code_module"

     2.1 --- a/etc/isar-keywords-ZF.el	Fri Oct 05 23:04:17 2007 +0200
     2.2 +++ b/etc/isar-keywords-ZF.el	Sat Oct 06 16:41:22 2007 +0200
     2.3 @@ -38,10 +38,13 @@
     2.4      "classrel"
     2.5      "codatatype"
     2.6      "code_datatype"
     2.7 +    "code_library"
     2.8 +    "code_module"
     2.9      "coinductive"
    2.10      "commit"
    2.11      "constdefs"
    2.12      "consts"
    2.13 +    "consts_code"
    2.14      "context"
    2.15      "corollary"
    2.16      "datatype"
    2.17 @@ -77,6 +80,8 @@
    2.18      "inductive_cases"
    2.19      "init_toplevel"
    2.20      "instance"
    2.21 +    "instance_proof"
    2.22 +    "instantiation"
    2.23      "interpret"
    2.24      "interpretation"
    2.25      "invoke"
    2.26 @@ -139,6 +144,8 @@
    2.27      "prop"
    2.28      "pwd"
    2.29      "qed"
    2.30 +    "quickcheck"
    2.31 +    "quickcheck_params"
    2.32      "quit"
    2.33      "realizability"
    2.34      "realizers"
    2.35 @@ -177,6 +184,7 @@
    2.36      "typed_print_translation"
    2.37      "typedecl"
    2.38      "types"
    2.39 +    "types_code"
    2.40      "ultimately"
    2.41      "undo"
    2.42      "undos_proof"
    2.43 @@ -184,6 +192,7 @@
    2.44      "use"
    2.45      "use_thy"
    2.46      "using"
    2.47 +    "value"
    2.48      "welcome"
    2.49      "with"
    2.50      "{"
    2.51 @@ -200,9 +209,11 @@
    2.52      "con_defs"
    2.53      "concl"
    2.54      "constrains"
    2.55 +    "contains"
    2.56      "defines"
    2.57      "domains"
    2.58      "elimination"
    2.59 +    "file"
    2.60      "fixes"
    2.61      "for"
    2.62      "identifier"
    2.63 @@ -216,6 +227,7 @@
    2.64      "infixr"
    2.65      "intros"
    2.66      "is"
    2.67 +    "local_syntax"
    2.68      "monos"
    2.69      "notes"
    2.70      "obtains"
    2.71 @@ -292,6 +304,7 @@
    2.72      "print_trans_rules"
    2.73      "prop"
    2.74      "pwd"
    2.75 +    "quickcheck"
    2.76      "remove_thy"
    2.77      "term"
    2.78      "thm"
    2.79 @@ -302,6 +315,7 @@
    2.80      "typ"
    2.81      "use"
    2.82      "use_thy"
    2.83 +    "value"
    2.84      "welcome"))
    2.85  
    2.86  (defconst isar-keywords-theory-begin
    2.87 @@ -331,9 +345,12 @@
    2.88      "classrel"
    2.89      "codatatype"
    2.90      "code_datatype"
    2.91 +    "code_library"
    2.92 +    "code_module"
    2.93      "coinductive"
    2.94      "constdefs"
    2.95      "consts"
    2.96 +    "consts_code"
    2.97      "context"
    2.98      "datatype"
    2.99      "declaration"
   2.100 @@ -347,6 +364,7 @@
   2.101      "global"
   2.102      "hide"
   2.103      "inductive"
   2.104 +    "instantiation"
   2.105      "judgment"
   2.106      "lemmas"
   2.107      "local"
   2.108 @@ -362,6 +380,7 @@
   2.109      "primrec"
   2.110      "print_ast_translation"
   2.111      "print_translation"
   2.112 +    "quickcheck_params"
   2.113      "realizability"
   2.114      "realizers"
   2.115      "rep_datatype"
   2.116 @@ -375,7 +394,8 @@
   2.117      "translations"
   2.118      "typed_print_translation"
   2.119      "typedecl"
   2.120 -    "types"))
   2.121 +    "types"
   2.122 +    "types_code"))
   2.123  
   2.124  (defconst isar-keywords-theory-script
   2.125    '("inductive_cases"))
   2.126 @@ -383,6 +403,7 @@
   2.127  (defconst isar-keywords-theory-goal
   2.128    '("corollary"
   2.129      "instance"
   2.130 +    "instance_proof"
   2.131      "interpretation"
   2.132      "lemma"
   2.133      "theorem"))

     3.1 --- a/etc/isar-keywords.el	Fri Oct 05 23:04:17 2007 +0200
     3.2 +++ b/etc/isar-keywords.el	Sat Oct 06 16:41:22 2007 +0200
     3.3 @@ -42,6 +42,7 @@
     3.4      "code_const"
     3.5      "code_datatype"
     3.6      "code_deps"
     3.7 +    "code_exception"
     3.8      "code_instance"
     3.9      "code_library"
    3.10      "code_module"
    3.11 @@ -268,6 +269,7 @@
    3.12      "internals"
    3.13      "is"
    3.14      "lazy"
    3.15 +    "local_syntax"
    3.16      "module_name"
    3.17      "monos"
    3.18      "morphisms"
    3.19 @@ -407,6 +409,7 @@
    3.20      "code_class"
    3.21      "code_const"
    3.22      "code_datatype"
    3.23 +    "code_exception"
    3.24      "code_instance"
    3.25      "code_library"
    3.26      "code_module"