1.1 --- a/etc/isar-keywords-HOL-Nominal.el	Thu Jan 18 11:16:49 2007 +0100
     1.2 +++ b/etc/isar-keywords-HOL-Nominal.el	Fri Jan 19 13:09:31 2007 +0100
     1.3 @@ -61,6 +61,7 @@
     1.4      "context"
     1.5      "corollary"
     1.6      "datatype"
     1.7 +    "declaration"
     1.8      "declare"
     1.9      "def"
    1.10      "defaultsort"
    1.11 @@ -395,6 +396,7 @@
    1.12      "consts_code"
    1.13      "context"
    1.14      "datatype"
    1.15 +    "declaration"
    1.16      "defaultsort"
    1.17      "defer_recdef"
    1.18      "definition"

     2.1 --- a/etc/isar-keywords-ZF.el	Thu Jan 18 11:16:49 2007 +0100
     2.2 +++ b/etc/isar-keywords-ZF.el	Fri Jan 19 13:09:31 2007 +0100
     2.3 @@ -58,6 +58,7 @@
     2.4      "context"
     2.5      "corollary"
     2.6      "datatype"
     2.7 +    "declaration"
     2.8      "declare"
     2.9      "def"
    2.10      "defaultsort"
    2.11 @@ -373,6 +374,7 @@
    2.12      "consts_code"
    2.13      "context"
    2.14      "datatype"
    2.15 +    "declaration"
    2.16      "defaultsort"
    2.17      "definition"
    2.18      "defs"

     3.1 --- a/etc/isar-keywords.el	Thu Jan 18 11:16:49 2007 +0100
     3.2 +++ b/etc/isar-keywords.el	Fri Jan 19 13:09:31 2007 +0100
     3.3 @@ -12,14 +12,11 @@
     3.4      "ML_command"
     3.5      "ML_setup"
     3.6      "ProofGeneral\\.call_atp"
     3.7 -    "ProofGeneral\\.context_thy_only"
     3.8      "ProofGeneral\\.inform_file_processed"
     3.9      "ProofGeneral\\.inform_file_retracted"
    3.10      "ProofGeneral\\.kill_proof"
    3.11      "ProofGeneral\\.process_pgip"
    3.12 -    "ProofGeneral\\.redo"
    3.13      "ProofGeneral\\.restart"
    3.14 -    "ProofGeneral\\.try_context_thy_only"
    3.15      "ProofGeneral\\.undo"
    3.16      "abbreviation"
    3.17      "also"
    3.18 @@ -42,7 +39,6 @@
    3.19      "class_deps"
    3.20      "classes"
    3.21      "classrel"
    3.22 -    "clear_undos"
    3.23      "code_abstype"
    3.24      "code_axioms"
    3.25      "code_class"
    3.26 @@ -53,6 +49,7 @@
    3.27      "code_module"
    3.28      "code_modulename"
    3.29      "code_moduleprolog"
    3.30 +    "code_monad"
    3.31      "code_reserved"
    3.32      "code_type"
    3.33      "coinductive"
    3.34 @@ -65,6 +62,7 @@
    3.35      "corollary"
    3.36      "cpodef"
    3.37      "datatype"
    3.38 +    "declaration"
    3.39      "declare"
    3.40      "def"
    3.41      "defaultsort"
    3.42 @@ -292,17 +290,13 @@
    3.43      "where"))
    3.44  
    3.45  (defconst isar-keywords-control
    3.46 -  '("ProofGeneral\\.context_thy_only"
    3.47 -    "ProofGeneral\\.inform_file_processed"
    3.48 +  '("ProofGeneral\\.inform_file_processed"
    3.49      "ProofGeneral\\.inform_file_retracted"
    3.50      "ProofGeneral\\.kill_proof"
    3.51      "ProofGeneral\\.process_pgip"
    3.52 -    "ProofGeneral\\.redo"
    3.53      "ProofGeneral\\.restart"
    3.54 -    "ProofGeneral\\.try_context_thy_only"
    3.55      "ProofGeneral\\.undo"
    3.56      "cannot_undo"
    3.57 -    "clear_undos"
    3.58      "exit"
    3.59      "init_toplevel"
    3.60      "kill"
    3.61 @@ -410,6 +404,7 @@
    3.62      "code_module"
    3.63      "code_modulename"
    3.64      "code_moduleprolog"
    3.65 +    "code_monad"
    3.66      "code_reserved"
    3.67      "code_type"
    3.68      "coinductive"
    3.69 @@ -419,6 +414,7 @@
    3.70      "consts_code"
    3.71      "context"
    3.72      "datatype"
    3.73 +    "declaration"
    3.74      "defaultsort"
    3.75      "defer_recdef"
    3.76      "definition"