--- 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"