1.1 --- a/etc/isar-keywords-HOL-Nominal.el	Tue Nov 07 11:28:25 2006 +0100
     1.2 +++ b/etc/isar-keywords-HOL-Nominal.el	Tue Nov 07 11:46:45 2006 +0100
     1.3 @@ -47,19 +47,17 @@
     1.4      "code_axioms"
     1.5      "code_class"
     1.6      "code_const"
     1.7 -    "code_constname"
     1.8      "code_gen"
     1.9      "code_instance"
    1.10 -    "code_instname"
    1.11      "code_library"
    1.12      "code_module"
    1.13 +    "code_modulename"
    1.14 +    "code_moduleprolog"
    1.15      "code_reserved"
    1.16      "code_type"
    1.17 -    "code_typename"
    1.18      "coinductive"
    1.19      "coinductive2"
    1.20      "commit"
    1.21 -    "const_syntax"
    1.22      "constdefs"
    1.23      "consts"
    1.24      "consts_code"
    1.25 @@ -120,6 +118,7 @@
    1.26      "nominal_datatype"
    1.27      "nonterminals"
    1.28      "normal_form"
    1.29 +    "notation"
    1.30      "note"
    1.31      "obtain"
    1.32      "oops"
    1.33 @@ -265,7 +264,6 @@
    1.34      "sequential"
    1.35      "shows"
    1.36      "structure"
    1.37 -    "target_atom"
    1.38      "unchecked"
    1.39      "uses"
    1.40      "where"))
    1.41 @@ -382,17 +380,15 @@
    1.42      "code_axioms"
    1.43      "code_class"
    1.44      "code_const"
    1.45 -    "code_constname"
    1.46      "code_instance"
    1.47 -    "code_instname"
    1.48      "code_library"
    1.49      "code_module"
    1.50 +    "code_modulename"
    1.51 +    "code_moduleprolog"
    1.52      "code_reserved"
    1.53      "code_type"
    1.54 -    "code_typename"
    1.55      "coinductive"
    1.56      "coinductive2"
    1.57 -    "const_syntax"
    1.58      "constdefs"
    1.59      "consts"
    1.60      "consts_code"
    1.61 @@ -418,6 +414,7 @@
    1.62      "no_translations"
    1.63      "nominal_datatype"
    1.64      "nonterminals"
    1.65 +    "notation"
    1.66      "oracle"
    1.67      "parse_ast_translation"
    1.68      "parse_translation"

     2.1 --- a/etc/isar-keywords-ZF.el	Tue Nov 07 11:28:25 2006 +0100
     2.2 +++ b/etc/isar-keywords-ZF.el	Tue Nov 07 11:46:45 2006 +0100
     2.3 @@ -45,18 +45,16 @@
     2.4      "code_axioms"
     2.5      "code_class"
     2.6      "code_const"
     2.7 -    "code_constname"
     2.8      "code_gen"
     2.9      "code_instance"
    2.10 -    "code_instname"
    2.11      "code_library"
    2.12      "code_module"
    2.13 +    "code_modulename"
    2.14 +    "code_moduleprolog"
    2.15      "code_reserved"
    2.16      "code_type"
    2.17 -    "code_typename"
    2.18      "coinductive"
    2.19      "commit"
    2.20 -    "const_syntax"
    2.21      "constdefs"
    2.22      "consts"
    2.23      "consts_code"
    2.24 @@ -111,6 +109,7 @@
    2.25      "no_translations"
    2.26      "nonterminals"
    2.27      "normal_form"
    2.28 +    "notation"
    2.29      "note"
    2.30      "obtain"
    2.31      "oops"
    2.32 @@ -246,7 +245,6 @@
    2.33      "recursor_eqns"
    2.34      "shows"
    2.35      "structure"
    2.36 -    "target_atom"
    2.37      "type_elims"
    2.38      "type_intros"
    2.39      "unchecked"
    2.40 @@ -364,16 +362,14 @@
    2.41      "code_axioms"
    2.42      "code_class"
    2.43      "code_const"
    2.44 -    "code_constname"
    2.45      "code_instance"
    2.46 -    "code_instname"
    2.47      "code_library"
    2.48      "code_module"
    2.49 +    "code_modulename"
    2.50 +    "code_moduleprolog"
    2.51      "code_reserved"
    2.52      "code_type"
    2.53 -    "code_typename"
    2.54      "coinductive"
    2.55 -    "const_syntax"
    2.56      "constdefs"
    2.57      "consts"
    2.58      "consts_code"
    2.59 @@ -395,6 +391,7 @@
    2.60      "no_syntax"
    2.61      "no_translations"
    2.62      "nonterminals"
    2.63 +    "notation"
    2.64      "oracle"
    2.65      "parse_ast_translation"
    2.66      "parse_translation"

     3.1 --- a/etc/isar-keywords.el	Tue Nov 07 11:28:25 2006 +0100
     3.2 +++ b/etc/isar-keywords.el	Tue Nov 07 11:46:45 2006 +0100
     3.3 @@ -47,19 +47,17 @@
     3.4      "code_axioms"
     3.5      "code_class"
     3.6      "code_const"
     3.7 -    "code_constname"
     3.8      "code_gen"
     3.9      "code_instance"
    3.10 -    "code_instname"
    3.11      "code_library"
    3.12      "code_module"
    3.13 +    "code_modulename"
    3.14 +    "code_moduleprolog"
    3.15      "code_reserved"
    3.16      "code_type"
    3.17 -    "code_typename"
    3.18      "coinductive"
    3.19      "coinductive2"
    3.20      "commit"
    3.21 -    "const_syntax"
    3.22      "constdefs"
    3.23      "consts"
    3.24      "consts_code"
    3.25 @@ -123,6 +121,7 @@
    3.26      "no_translations"
    3.27      "nonterminals"
    3.28      "normal_form"
    3.29 +    "notation"
    3.30      "note"
    3.31      "obtain"
    3.32      "oops"
    3.33 @@ -283,7 +282,6 @@
    3.34      "signature"
    3.35      "states"
    3.36      "structure"
    3.37 -    "target_atom"
    3.38      "to"
    3.39      "transitions"
    3.40      "transrel"
    3.41 @@ -403,17 +401,15 @@
    3.42      "code_axioms"
    3.43      "code_class"
    3.44      "code_const"
    3.45 -    "code_constname"
    3.46      "code_instance"
    3.47 -    "code_instname"
    3.48      "code_library"
    3.49      "code_module"
    3.50 +    "code_modulename"
    3.51 +    "code_moduleprolog"
    3.52      "code_reserved"
    3.53      "code_type"
    3.54 -    "code_typename"
    3.55      "coinductive"
    3.56      "coinductive2"
    3.57 -    "const_syntax"
    3.58      "constdefs"
    3.59      "consts"
    3.60      "consts_code"
    3.61 @@ -441,6 +437,7 @@
    3.62      "no_syntax"
    3.63      "no_translations"
    3.64      "nonterminals"
    3.65 +    "notation"
    3.66      "oracle"
    3.67      "parse_ast_translation"
    3.68      "parse_translation"