# HG changeset patch
# User haftmann
# Date 1150280209 -7200
# Node ID 2857fac35e6d9f06538c7bff7945cd4a0e51501f
# Parent  1aad48bcc674e9797719fed1d1740502afdd7739
keyword update

diff -r 1aad48bcc674 -r 2857fac35e6d etc/isar-keywords-HOL-Nominal.el
--- 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"
diff -r 1aad48bcc674 -r 2857fac35e6d etc/isar-keywords-ZF.el
--- 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"
diff -r 1aad48bcc674 -r 2857fac35e6d etc/isar-keywords.el
--- 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"