Mercurial Mercurial > hg > nominal2 / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
added a print_maps command; updated the keyword file accordingly
authorChristian Urban <urbanc@in.tum.de>
Tue, 22 Dec 2009 21:44:50 +0100
changeset 777 2f72662d21f3
parent 776 d1064fa29424
child 778 54f186bb5e3e
added a print_maps command; updated the keyword file accordingly
Quot/quotient_info.ML file | annotate | diff | comparison | revisions
isar-keywords-quot.el file | annotate | diff | comparison | revisions 
--- 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
 
--- 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"
nominal2