Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
updated keywords
authorhaftmann
Tue, 16 Jan 2007 08:06:52 +0100
changeset 22066 78b151461b89
parent 22065 cdd077905eee
child 22067 39d5d42116c4
updated keywords
etc/isar-keywords-HOL-Nominal.el file | annotate | diff | comparison | revisions
etc/isar-keywords-ZF.el file | annotate | diff | comparison | revisions 
--- 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"
--- 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"
isabelle