changeset 784 | da75568e7f12 |
parent 768 | e9e205b904e2 |
child 787 | 5cf83fa5b36c |
--- a/Quot/Examples/FSet3.thy Wed Dec 23 22:42:30 2009 +0100 +++ b/Quot/Examples/FSet3.thy Wed Dec 23 23:22:02 2009 +0100 @@ -12,6 +12,8 @@ unfolding equivp_reflp_symp_transp reflp_def symp_def transp_def by auto +(* FIXME-TODO: because of beta-reduction, one cannot give the *) +(* FIXME-TODO: relation as a term or abbreviation *) quotient_type fset = "'a list" / "list_eq" by (rule list_eq_equivp)