changeset 787 | 5cf83fa5b36c |
parent 784 | da75568e7f12 |
child 793 | 09dff5ef8f74 |
--- a/Quot/Examples/FSet3.thy Thu Dec 24 00:58:50 2009 +0100 +++ b/Quot/Examples/FSet3.thy Thu Dec 24 22:28:19 2009 +0100 @@ -15,7 +15,7 @@ (* 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" + 'a fset = "'a list" / "list_eq" by (rule list_eq_equivp)