equal
deleted
inserted
replaced
10 lemma list_eq_equivp: |
10 lemma list_eq_equivp: |
11 shows "equivp list_eq" |
11 shows "equivp list_eq" |
12 unfolding equivp_reflp_symp_transp reflp_def symp_def transp_def |
12 unfolding equivp_reflp_symp_transp reflp_def symp_def transp_def |
13 by auto |
13 by auto |
14 |
14 |
|
15 (* FIXME-TODO: because of beta-reduction, one cannot give the *) |
|
16 (* FIXME-TODO: relation as a term or abbreviation *) |
15 quotient_type |
17 quotient_type |
16 fset = "'a list" / "list_eq" |
18 fset = "'a list" / "list_eq" |
17 by (rule list_eq_equivp) |
19 by (rule list_eq_equivp) |
18 |
20 |
19 |
21 |