# HG changeset patch
# User wenzelm
# Date 1169208571 -3600
# Node ID 2fef69700f50bd91f4edeb851d861ead286d89fd
# Parent  4bfd987b005c7bec05f8066b0e0b370064ca784d
updated

diff -r 4bfd987b005c -r 2fef69700f50 etc/isar-keywords-HOL-Nominal.el
--- a/etc/isar-keywords-HOL-Nominal.el	Thu Jan 18 11:16:49 2007 +0100
+++ b/etc/isar-keywords-HOL-Nominal.el	Fri Jan 19 13:09:31 2007 +0100
@@ -61,6 +61,7 @@
     "context"
     "corollary"
     "datatype"
+    "declaration"
     "declare"
     "def"
     "defaultsort"
@@ -395,6 +396,7 @@
     "consts_code"
     "context"
     "datatype"
+    "declaration"
     "defaultsort"
     "defer_recdef"
     "definition"
diff -r 4bfd987b005c -r 2fef69700f50 etc/isar-keywords-ZF.el
--- a/etc/isar-keywords-ZF.el	Thu Jan 18 11:16:49 2007 +0100
+++ b/etc/isar-keywords-ZF.el	Fri Jan 19 13:09:31 2007 +0100
@@ -58,6 +58,7 @@
     "context"
     "corollary"
     "datatype"
+    "declaration"
     "declare"
     "def"
     "defaultsort"
@@ -373,6 +374,7 @@
     "consts_code"
     "context"
     "datatype"
+    "declaration"
     "defaultsort"
     "definition"
     "defs"
diff -r 4bfd987b005c -r 2fef69700f50 etc/isar-keywords.el
--- a/etc/isar-keywords.el	Thu Jan 18 11:16:49 2007 +0100
+++ b/etc/isar-keywords.el	Fri Jan 19 13:09:31 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"
@@ -65,6 +62,7 @@
     "corollary"
     "cpodef"
     "datatype"
+    "declaration"
     "declare"
     "def"
     "defaultsort"
@@ -292,17 +290,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"
@@ -410,6 +404,7 @@
     "code_module"
     "code_modulename"
     "code_moduleprolog"
+    "code_monad"
     "code_reserved"
     "code_type"
     "coinductive"
@@ -419,6 +414,7 @@
     "consts_code"
     "context"
     "datatype"
+    "declaration"
     "defaultsort"
     "defer_recdef"
     "definition"