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
authorwenzelm
Fri, 19 Jan 2007 13:09:31 +0100
changeset 22084 2fef69700f50
parent 22083 4bfd987b005c
child 22085 c138cfd500f7
updated
etc/isar-keywords-HOL-Nominal.el file | annotate | diff | comparison | revisions
etc/isar-keywords-ZF.el file | annotate | diff | comparison | revisions
etc/isar-keywords.el file | annotate | diff | comparison | revisions 
--- 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"
--- 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"
--- 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"
isabelle