--- a/etc/isar-keywords-ZF.el Mon Feb 22 09:36:47 2010 +0100
+++ b/etc/isar-keywords-ZF.el Mon Feb 22 10:38:58 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 09:36:47 2010 +0100
+++ b/etc/isar-keywords.el Mon Feb 22 10:38:58 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"
--- a/src/HOL/Tools/Quotient/quotient_info.ML Mon Feb 22 09:36:47 2010 +0100
+++ b/src/HOL/Tools/Quotient/quotient_info.ML Mon Feb 22 10:38:58 2010 +0100
@@ -280,7 +280,7 @@
OuterKeyword.diag (Scan.succeed (Toplevel.keep (pp_fn o Toplevel.context_of)))
val _ = map improper_command
- [(print_mapsinfo, "print_maps", "prints out all map functions"),
+ [(print_mapsinfo, "print_quotmaps", "prints out all map functions"),
(print_quotinfo, "print_quotients", "prints out all quotients"),
(print_qconstinfo, "print_quotconsts", "prints out all quotient constants")]