# HG changeset patch
# User Christian Urban <urbanc@in.tum.de>
# Date 1261514690 -3600
# Node ID 2f72662d21f350198f9f2936cd03a86f1ec70e8a
# Parent  d1064fa29424d1cc84dade9b530c0a27474d9451
added a print_maps command; updated the keyword file accordingly

diff -r d1064fa29424 -r 2f72662d21f3 Quot/quotient_info.ML
--- a/Quot/quotient_info.ML	Tue Dec 22 21:31:44 2009 +0100
+++ b/Quot/quotient_info.ML	Tue Dec 22 21:44:50 2009 +0100
@@ -38,6 +38,7 @@
 
 exception NotFound
 
+(*******************)
 (* data containers *)
 (*******************)
 
@@ -103,6 +104,9 @@
   |> Pretty.writeln
 end
 
+val _ = 
+  OuterSyntax.improper_command "print_maps" "prints out all map functions" 
+    OuterKeyword.diag (Scan.succeed (Toplevel.keep (print_mapsinfo o Toplevel.context_of)))
 
 
 (* info about quotient types *)
@@ -149,7 +153,7 @@
 end
 
 val _ = 
-  OuterSyntax.improper_command "print_quotients" "print out all quotients" 
+  OuterSyntax.improper_command "print_quotients" "prints out all quotients" 
     OuterKeyword.diag (Scan.succeed (Toplevel.keep (print_quotinfo o Toplevel.context_of)))
 
 
@@ -209,7 +213,7 @@
 end
 
 val _ = 
-  OuterSyntax.improper_command "print_quotconsts" "print out all quotient constants" 
+  OuterSyntax.improper_command "print_quotconsts" "prints out all quotient constants" 
     OuterKeyword.diag (Scan.succeed (Toplevel.keep (print_qconstinfo o Toplevel.context_of)))
 
 (* FIXME/TODO: check the various lemmas conform *)
@@ -233,7 +237,7 @@
 (* preservation theorems *)
 structure PrsRules = Named_Thms
   (val name = "quot_preserve"
-   val description = "Respectfulness theorems.")
+   val description = "Preservation theorems.")
 
 val prs_rules_get = PrsRules.get
 
diff -r d1064fa29424 -r 2f72662d21f3 isar-keywords-quot.el
--- a/isar-keywords-quot.el	Tue Dec 22 21:31:44 2009 +0100
+++ b/isar-keywords-quot.el	Tue Dec 22 21:44:50 2009 +0100
@@ -173,6 +173,7 @@
     "print_interps"
     "print_locale"
     "print_locales"
+    "print_maps"
     "print_methods"
     "print_orders"
     "print_quotconsts"
@@ -365,6 +366,7 @@
     "print_interps"
     "print_locale"
     "print_locales"
+    "print_maps"
     "print_methods"
     "print_orders"
     "print_quotconsts"