etc/isar-keywords-ZF.el
changeset 22066 78b151461b89
parent 21806 6086783d4214
child 22084 2fef69700f50
--- 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"