changeset 786 | d6407afb913c |
parent 783 | 06e17083e90b |
child 787 | 5cf83fa5b36c |
--- 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" / "\<lambda>(xs::'a list) ys. \<forall>e. e \<in> set xs \<longleftrightarrow> e \<in> set ys" apply(rule equivpI)