1.1 --- a/etc/isar-keywords-HOL-Nominal.el	Fri Oct 13 18:33:50 2006 +0200
     1.2 +++ b/etc/isar-keywords-HOL-Nominal.el	Fri Oct 13 22:30:29 2006 +0200
     1.3 @@ -53,9 +53,11 @@
     1.4      "code_instname"
     1.5      "code_library"
     1.6      "code_module"
     1.7 +    "code_reserved"
     1.8      "code_type"
     1.9      "code_typename"
    1.10      "coinductive"
    1.11 +    "coinductive2"
    1.12      "commit"
    1.13      "const_syntax"
    1.14      "constdefs"
    1.15 @@ -94,7 +96,9 @@
    1.16      "hence"
    1.17      "hide"
    1.18      "inductive"
    1.19 +    "inductive2"
    1.20      "inductive_cases"
    1.21 +    "inductive_cases2"
    1.22      "init_toplevel"
    1.23      "instance"
    1.24      "interpret"
    1.25 @@ -207,7 +211,6 @@
    1.26      "types_code"
    1.27      "ultimately"
    1.28      "undo"
    1.29 -    "undo_end"
    1.30      "undos_proof"
    1.31      "unfolding"
    1.32      "update_thy"
    1.33 @@ -285,7 +288,6 @@
    1.34      "quit"
    1.35      "redo"
    1.36      "undo"
    1.37 -    "undo_end"
    1.38      "undos_proof"))
    1.39  
    1.40  (defconst isar-keywords-diag
    1.41 @@ -385,9 +387,11 @@
    1.42      "code_instname"
    1.43      "code_library"
    1.44      "code_module"
    1.45 +    "code_reserved"
    1.46      "code_type"
    1.47      "code_typename"
    1.48      "coinductive"
    1.49 +    "coinductive2"
    1.50      "const_syntax"
    1.51      "constdefs"
    1.52      "consts"
    1.53 @@ -404,6 +408,7 @@
    1.54      "global"
    1.55      "hide"
    1.56      "inductive"
    1.57 +    "inductive2"
    1.58      "judgment"
    1.59      "lemmas"
    1.60      "local"
    1.61 @@ -440,7 +445,8 @@
    1.62  
    1.63  (defconst isar-keywords-theory-script
    1.64    '("declare"
    1.65 -    "inductive_cases"))
    1.66 +    "inductive_cases"
    1.67 +    "inductive_cases2"))
    1.68  
    1.69  (defconst isar-keywords-theory-goal
    1.70    '("ax_specification"

     2.1 --- a/etc/isar-keywords-ZF.el	Fri Oct 13 18:33:50 2006 +0200
     2.2 +++ b/etc/isar-keywords-ZF.el	Fri Oct 13 22:30:29 2006 +0200
     2.3 @@ -51,6 +51,7 @@
     2.4      "code_instname"
     2.5      "code_library"
     2.6      "code_module"
     2.7 +    "code_reserved"
     2.8      "code_type"
     2.9      "code_typename"
    2.10      "coinductive"
    2.11 @@ -194,7 +195,6 @@
    2.12      "types_code"
    2.13      "ultimately"
    2.14      "undo"
    2.15 -    "undo_end"
    2.16      "undos_proof"
    2.17      "unfolding"
    2.18      "update_thy"
    2.19 @@ -271,7 +271,6 @@
    2.20      "quit"
    2.21      "redo"
    2.22      "undo"
    2.23 -    "undo_end"
    2.24      "undos_proof"))
    2.25  
    2.26  (defconst isar-keywords-diag
    2.27 @@ -370,6 +369,7 @@
    2.28      "code_instname"
    2.29      "code_library"
    2.30      "code_module"
    2.31 +    "code_reserved"
    2.32      "code_type"
    2.33      "code_typename"
    2.34      "coinductive"

     3.1 --- a/etc/isar-keywords.el	Fri Oct 13 18:33:50 2006 +0200
     3.2 +++ b/etc/isar-keywords.el	Fri Oct 13 22:30:29 2006 +0200
     3.3 @@ -53,6 +53,7 @@
     3.4      "code_instname"
     3.5      "code_library"
     3.6      "code_module"
     3.7 +    "code_reserved"
     3.8      "code_type"
     3.9      "code_typename"
    3.10      "coinductive"
    3.11 @@ -407,6 +408,7 @@
    3.12      "code_instname"
    3.13      "code_library"
    3.14      "code_module"
    3.15 +    "code_reserved"
    3.16      "code_type"
    3.17      "code_typename"
    3.18      "coinductive"