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.
keyword update
authorhaftmann
Wed, 14 Jun 2006 12:16:49 +0200
changeset 19891 2857fac35e6d
parent 19890 1aad48bcc674
child 19892 e41ef99d9bb3
keyword update
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	Wed Jun 14 12:14:42 2006 +0200
+++ b/etc/isar-keywords-HOL-Nominal.el	Wed Jun 14 12:16:49 2006 +0200
@@ -43,13 +43,15 @@
     "classrel"
     "clear_undos"
     "code_alias"
+    "code_classapp"
+    "code_constapp"
     "code_generate"
     "code_library"
     "code_module"
     "code_purge"
     "code_serialize"
-    "code_syntax_const"
-    "code_syntax_tyco"
+    "code_simtype"
+    "code_typapp"
     "coinductive"
     "commit"
     "const_syntax"
@@ -360,13 +362,14 @@
     "classes"
     "classrel"
     "code_alias"
+    "code_classapp"
+    "code_constapp"
     "code_generate"
     "code_library"
     "code_module"
     "code_purge"
     "code_serialize"
-    "code_syntax_const"
-    "code_syntax_tyco"
+    "code_typapp"
     "coinductive"
     "const_syntax"
     "constdefs"
@@ -424,6 +427,7 @@
 
 (defconst isar-keywords-theory-goal
   '("ax_specification"
+    "code_simtype"
     "corollary"
     "function"
     "instance"
--- a/etc/isar-keywords-ZF.el	Wed Jun 14 12:14:42 2006 +0200
+++ b/etc/isar-keywords-ZF.el	Wed Jun 14 12:16:49 2006 +0200
@@ -41,13 +41,15 @@
     "clear_undos"
     "codatatype"
     "code_alias"
+    "code_classapp"
+    "code_constapp"
     "code_generate"
     "code_library"
     "code_module"
     "code_purge"
     "code_serialize"
-    "code_syntax_const"
-    "code_syntax_tyco"
+    "code_simtype"
+    "code_typapp"
     "coinductive"
     "commit"
     "const_syntax"
@@ -348,13 +350,14 @@
     "classrel"
     "codatatype"
     "code_alias"
+    "code_classapp"
+    "code_constapp"
     "code_generate"
     "code_library"
     "code_module"
     "code_purge"
     "code_serialize"
-    "code_syntax_const"
-    "code_syntax_tyco"
+    "code_typapp"
     "coinductive"
     "const_syntax"
     "constdefs"
@@ -406,7 +409,8 @@
     "inductive_cases"))
 
 (defconst isar-keywords-theory-goal
-  '("corollary"
+  '("code_simtype"
+    "corollary"
     "instance"
     "interpretation"
     "lemma"
--- a/etc/isar-keywords.el	Wed Jun 14 12:14:42 2006 +0200
+++ b/etc/isar-keywords.el	Wed Jun 14 12:16:49 2006 +0200
@@ -43,13 +43,15 @@
     "classrel"
     "clear_undos"
     "code_alias"
+    "code_classapp"
+    "code_constapp"
     "code_generate"
     "code_library"
     "code_module"
     "code_purge"
     "code_serialize"
-    "code_syntax_const"
-    "code_syntax_tyco"
+    "code_simtype"
+    "code_typapp"
     "coinductive"
     "commit"
     "const_syntax"
@@ -381,13 +383,14 @@
     "classes"
     "classrel"
     "code_alias"
+    "code_classapp"
+    "code_constapp"
     "code_generate"
     "code_library"
     "code_module"
     "code_purge"
     "code_serialize"
-    "code_syntax_const"
-    "code_syntax_tyco"
+    "code_typapp"
     "coinductive"
     "const_syntax"
     "constdefs"
@@ -447,6 +450,7 @@
 
 (defconst isar-keywords-theory-goal
   '("ax_specification"
+    "code_simtype"
     "corollary"
     "cpodef"
     "function"
isabelle