update the keywords files
authorCezary Kaliszyk <kaliszyk@in.tum.de>
Mon, 22 Feb 2010 10:28:49 +0100
changeset 35279 4f6760122b2a
parent 35278 a5d0bfcaf26a
child 35280 54ab4921f826
child 35298 71bca9e4c483
child 35299 4f4d5bf4ea08
update the keywords files
etc/isar-keywords-ZF.el
etc/isar-keywords.el
--- a/etc/isar-keywords-ZF.el	Mon Feb 22 10:28:00 2010 +0100
+++ b/etc/isar-keywords-ZF.el	Mon Feb 22 10:28:49 2010 +0100
@@ -44,6 +44,7 @@
     "classes"
     "classrel"
     "codatatype"
+    "code_abstype"
     "code_datatype"
     "code_library"
     "code_module"
@@ -413,7 +414,8 @@
   '("inductive_cases"))
 
 (defconst isar-keywords-theory-goal
-  '("corollary"
+  '("code_abstype"
+    "corollary"
     "instance"
     "interpretation"
     "lemma"
--- a/etc/isar-keywords.el	Mon Feb 22 10:28:00 2010 +0100
+++ b/etc/isar-keywords.el	Mon Feb 22 10:28:49 2010 +0100
@@ -188,6 +188,9 @@
     "print_locales"
     "print_methods"
     "print_orders"
+    "print_quotconsts"
+    "print_quotients"
+    "print_quotmaps"
     "print_rules"
     "print_simpset"
     "print_statement"
@@ -203,6 +206,8 @@
     "quickcheck"
     "quickcheck_params"
     "quit"
+    "quotient_definition"
+    "quotient_type"
     "realizability"
     "realizers"
     "recdef"
@@ -395,6 +400,9 @@
     "print_locales"
     "print_methods"
     "print_orders"
+    "print_quotconsts"
+    "print_quotients"
+    "print_quotmaps"
     "print_rules"
     "print_simpset"
     "print_statement"
@@ -512,6 +520,7 @@
     "print_ast_translation"
     "print_translation"
     "quickcheck_params"
+    "quotient_definition"
     "realizability"
     "realizers"
     "recdef"
@@ -550,6 +559,7 @@
     "nominal_inductive2"
     "nominal_primrec"
     "pcpodef"
+    "quotient_type"
     "recdef_tc"
     "rep_datatype"
     "specification"