Quot/Examples/AbsRepTest.thy
changeset 783 06e17083e90b
parent 780 a24e26f5488c
child 786 d6407afb913c
--- a/Quot/Examples/AbsRepTest.thy	Wed Dec 23 21:30:23 2009 +0100
+++ b/Quot/Examples/AbsRepTest.thy	Wed Dec 23 22:42:30 2009 +0100
@@ -9,6 +9,12 @@
   apply(auto)
   done
 
+print_quotients
+
+ML{*
+Quotient_Info.quotient_rules_get @{context}
+*}
+
 fun
   intrel :: "(nat \<times> nat) \<Rightarrow> (nat \<times> nat) \<Rightarrow> bool"
 where
@@ -17,6 +23,8 @@
 quotient_type int = "nat \<times> nat" / intrel
   sorry
 
+print_quotients
+
 ML {*
 open Quotient_Term;
 *}