diff -r bf6861ee3b90 -r d6407afb913c Quot/Examples/AbsRepTest.thy --- a/Quot/Examples/AbsRepTest.thy Wed Dec 23 23:53:03 2009 +0100 +++ b/Quot/Examples/AbsRepTest.thy Thu Dec 24 00:58:50 2009 +0100 @@ -2,6 +2,8 @@ imports "../QuotMain" "../QuotList" "../QuotOption" "../QuotSum" "../QuotProd" List begin +print_maps + quotient_type fset = "'a list" / "\(xs::'a list) ys. \e. e \ set xs \ e \ set ys" apply(rule equivpI)