1.1 --- a/etc/isar-keywords-HOL-Nominal.el	Mon Jan 15 10:15:55 2007 +0100
     1.2 +++ b/etc/isar-keywords-HOL-Nominal.el	Tue Jan 16 08:06:52 2007 +0100
     1.3 @@ -12,14 +12,11 @@
     1.4      "ML_command"
     1.5      "ML_setup"
     1.6      "ProofGeneral\\.call_atp"
     1.7 -    "ProofGeneral\\.context_thy_only"
     1.8      "ProofGeneral\\.inform_file_processed"
     1.9      "ProofGeneral\\.inform_file_retracted"
    1.10      "ProofGeneral\\.kill_proof"
    1.11      "ProofGeneral\\.process_pgip"
    1.12 -    "ProofGeneral\\.redo"
    1.13      "ProofGeneral\\.restart"
    1.14 -    "ProofGeneral\\.try_context_thy_only"
    1.15      "ProofGeneral\\.undo"
    1.16      "abbreviation"
    1.17      "also"
    1.18 @@ -42,7 +39,6 @@
    1.19      "class_deps"
    1.20      "classes"
    1.21      "classrel"
    1.22 -    "clear_undos"
    1.23      "code_abstype"
    1.24      "code_axioms"
    1.25      "code_class"
    1.26 @@ -53,6 +49,7 @@
    1.27      "code_module"
    1.28      "code_modulename"
    1.29      "code_moduleprolog"
    1.30 +    "code_monad"
    1.31      "code_reserved"
    1.32      "code_type"
    1.33      "coinductive"
    1.34 @@ -274,17 +271,13 @@
    1.35      "where"))
    1.36  
    1.37  (defconst isar-keywords-control
    1.38 -  '("ProofGeneral\\.context_thy_only"
    1.39 -    "ProofGeneral\\.inform_file_processed"
    1.40 +  '("ProofGeneral\\.inform_file_processed"
    1.41      "ProofGeneral\\.inform_file_retracted"
    1.42      "ProofGeneral\\.kill_proof"
    1.43      "ProofGeneral\\.process_pgip"
    1.44 -    "ProofGeneral\\.redo"
    1.45      "ProofGeneral\\.restart"
    1.46 -    "ProofGeneral\\.try_context_thy_only"
    1.47      "ProofGeneral\\.undo"
    1.48      "cannot_undo"
    1.49 -    "clear_undos"
    1.50      "exit"
    1.51      "init_toplevel"
    1.52      "kill"
    1.53 @@ -392,6 +385,7 @@
    1.54      "code_module"
    1.55      "code_modulename"
    1.56      "code_moduleprolog"
    1.57 +    "code_monad"
    1.58      "code_reserved"
    1.59      "code_type"
    1.60      "coinductive"

     2.1 --- a/etc/isar-keywords-ZF.el	Mon Jan 15 10:15:55 2007 +0100
     2.2 +++ b/etc/isar-keywords-ZF.el	Tue Jan 16 08:06:52 2007 +0100
     2.3 @@ -11,14 +11,11 @@
     2.4      "ML"
     2.5      "ML_command"
     2.6      "ML_setup"
     2.7 -    "ProofGeneral\\.context_thy_only"
     2.8      "ProofGeneral\\.inform_file_processed"
     2.9      "ProofGeneral\\.inform_file_retracted"
    2.10      "ProofGeneral\\.kill_proof"
    2.11      "ProofGeneral\\.process_pgip"
    2.12 -    "ProofGeneral\\.redo"
    2.13      "ProofGeneral\\.restart"
    2.14 -    "ProofGeneral\\.try_context_thy_only"
    2.15      "ProofGeneral\\.undo"
    2.16      "abbreviation"
    2.17      "also"
    2.18 @@ -39,7 +36,6 @@
    2.19      "class_deps"
    2.20      "classes"
    2.21      "classrel"
    2.22 -    "clear_undos"
    2.23      "codatatype"
    2.24      "code_abstype"
    2.25      "code_axioms"
    2.26 @@ -51,6 +47,7 @@
    2.27      "code_module"
    2.28      "code_modulename"
    2.29      "code_moduleprolog"
    2.30 +    "code_monad"
    2.31      "code_reserved"
    2.32      "code_type"
    2.33      "coinductive"
    2.34 @@ -254,17 +251,13 @@
    2.35      "where"))
    2.36  
    2.37  (defconst isar-keywords-control
    2.38 -  '("ProofGeneral\\.context_thy_only"
    2.39 -    "ProofGeneral\\.inform_file_processed"
    2.40 +  '("ProofGeneral\\.inform_file_processed"
    2.41      "ProofGeneral\\.inform_file_retracted"
    2.42      "ProofGeneral\\.kill_proof"
    2.43      "ProofGeneral\\.process_pgip"
    2.44 -    "ProofGeneral\\.redo"
    2.45      "ProofGeneral\\.restart"
    2.46 -    "ProofGeneral\\.try_context_thy_only"
    2.47      "ProofGeneral\\.undo"
    2.48      "cannot_undo"
    2.49 -    "clear_undos"
    2.50      "exit"
    2.51      "init_toplevel"
    2.52      "kill"
    2.53 @@ -371,6 +364,7 @@
    2.54      "code_module"
    2.55      "code_modulename"
    2.56      "code_moduleprolog"
    2.57 +    "code_monad"
    2.58      "code_reserved"
    2.59      "code_type"
    2.60      "coinductive"