# HG changeset patch
# User haftmann
# Date 1168931212 -3600
# Node ID 78b151461b89a5a017aab27d605f3eeaa383738c
# Parent  cdd077905eee9136bbac118c013bf74e623a6e02
updated keywords

diff -r cdd077905eee -r 78b151461b89 etc/isar-keywords-HOL-Nominal.el
--- a/etc/isar-keywords-HOL-Nominal.el	Mon Jan 15 10:15:55 2007 +0100
+++ b/etc/isar-keywords-HOL-Nominal.el	Tue Jan 16 08:06:52 2007 +0100
@@ -12,14 +12,11 @@
     "ML_command"
     "ML_setup"
     "ProofGeneral\\.call_atp"
-    "ProofGeneral\\.context_thy_only"
     "ProofGeneral\\.inform_file_processed"
     "ProofGeneral\\.inform_file_retracted"
     "ProofGeneral\\.kill_proof"
     "ProofGeneral\\.process_pgip"
-    "ProofGeneral\\.redo"
     "ProofGeneral\\.restart"
-    "ProofGeneral\\.try_context_thy_only"
     "ProofGeneral\\.undo"
     "abbreviation"
     "also"
@@ -42,7 +39,6 @@
     "class_deps"
     "classes"
     "classrel"
-    "clear_undos"
     "code_abstype"
     "code_axioms"
     "code_class"
@@ -53,6 +49,7 @@
     "code_module"
     "code_modulename"
     "code_moduleprolog"
+    "code_monad"
     "code_reserved"
     "code_type"
     "coinductive"
@@ -274,17 +271,13 @@
     "where"))
 
 (defconst isar-keywords-control
-  '("ProofGeneral\\.context_thy_only"
-    "ProofGeneral\\.inform_file_processed"
+  '("ProofGeneral\\.inform_file_processed"
     "ProofGeneral\\.inform_file_retracted"
     "ProofGeneral\\.kill_proof"
     "ProofGeneral\\.process_pgip"
-    "ProofGeneral\\.redo"
     "ProofGeneral\\.restart"
-    "ProofGeneral\\.try_context_thy_only"
     "ProofGeneral\\.undo"
     "cannot_undo"
-    "clear_undos"
     "exit"
     "init_toplevel"
     "kill"
@@ -392,6 +385,7 @@
     "code_module"
     "code_modulename"
     "code_moduleprolog"
+    "code_monad"
     "code_reserved"
     "code_type"
     "coinductive"
diff -r cdd077905eee -r 78b151461b89 etc/isar-keywords-ZF.el
--- a/etc/isar-keywords-ZF.el	Mon Jan 15 10:15:55 2007 +0100
+++ b/etc/isar-keywords-ZF.el	Tue Jan 16 08:06:52 2007 +0100
@@ -11,14 +11,11 @@
     "ML"
     "ML_command"
     "ML_setup"
-    "ProofGeneral\\.context_thy_only"
     "ProofGeneral\\.inform_file_processed"
     "ProofGeneral\\.inform_file_retracted"
     "ProofGeneral\\.kill_proof"
     "ProofGeneral\\.process_pgip"
-    "ProofGeneral\\.redo"
     "ProofGeneral\\.restart"
-    "ProofGeneral\\.try_context_thy_only"
     "ProofGeneral\\.undo"
     "abbreviation"
     "also"
@@ -39,7 +36,6 @@
     "class_deps"
     "classes"
     "classrel"
-    "clear_undos"
     "codatatype"
     "code_abstype"
     "code_axioms"
@@ -51,6 +47,7 @@
     "code_module"
     "code_modulename"
     "code_moduleprolog"
+    "code_monad"
     "code_reserved"
     "code_type"
     "coinductive"
@@ -254,17 +251,13 @@
     "where"))
 
 (defconst isar-keywords-control
-  '("ProofGeneral\\.context_thy_only"
-    "ProofGeneral\\.inform_file_processed"
+  '("ProofGeneral\\.inform_file_processed"
     "ProofGeneral\\.inform_file_retracted"
     "ProofGeneral\\.kill_proof"
     "ProofGeneral\\.process_pgip"
-    "ProofGeneral\\.redo"
     "ProofGeneral\\.restart"
-    "ProofGeneral\\.try_context_thy_only"
     "ProofGeneral\\.undo"
     "cannot_undo"
-    "clear_undos"
     "exit"
     "init_toplevel"
     "kill"
@@ -371,6 +364,7 @@
     "code_module"
     "code_modulename"
     "code_moduleprolog"
+    "code_monad"
     "code_reserved"
     "code_type"
     "coinductive"