diff -r 86c7ed9f354f -r 06e17083e90b Quot/Examples/AbsRepTest.thy --- 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 \ nat) \ (nat \ nat) \ bool" where @@ -17,6 +23,8 @@ quotient_type int = "nat \ nat" / intrel sorry +print_quotients + ML {* open Quotient_Term; *}