equal
deleted
inserted
replaced
13 by auto |
13 by auto |
14 |
14 |
15 (* FIXME-TODO: because of beta-reduction, one cannot give the *) |
15 (* FIXME-TODO: because of beta-reduction, one cannot give the *) |
16 (* FIXME-TODO: relation as a term or abbreviation *) |
16 (* FIXME-TODO: relation as a term or abbreviation *) |
17 quotient_type |
17 quotient_type |
18 fset = "'a list" / "list_eq" |
18 'a fset = "'a list" / "list_eq" |
19 by (rule list_eq_equivp) |
19 by (rule list_eq_equivp) |
20 |
20 |
21 |
21 |
22 section {* empty fset, finsert and membership *} |
22 section {* empty fset, finsert and membership *} |
23 |
23 |