1 theory AbsRepTest

     1 theory AbsRepTest

     2 imports "../QuotMain" "../QuotList" "../QuotOption" "../QuotSum" "../QuotProd" List

     2 imports "../QuotMain" "../QuotList" "../QuotOption" "../QuotSum" "../QuotProd" List

     3 begin

     3 begin

     4 

     6 

     5 quotient_type 

     7 quotient_type 

     6   fset = "'a list" / "\<lambda>(xs::'a list) ys. \<forall>e. e \<in> set xs \<longleftrightarrow> e \<in> set ys" 

     8   fset = "'a list" / "\<lambda>(xs::'a list) ys. \<forall>e. e \<in> set xs \<longleftrightarrow> e \<in> set ys" 

     7   apply(rule equivpI)

     9   apply(rule equivpI)

     8   unfolding reflp_def symp_def transp_def

    10   unfolding reflp_def symp_def transp_def