Quot/Examples/FSet3.thy
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)