
diff -r 06e17083e90b -r da75568e7f12 Quot/Examples/FSet3.thy
--- 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)




