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; *}