equal
deleted
inserted
replaced
19 lemma equivp_list_eq: |
19 lemma equivp_list_eq: |
20 shows "equivp list_eq" |
20 shows "equivp list_eq" |
21 unfolding equivp_reflp_symp_transp reflp_def symp_def transp_def |
21 unfolding equivp_reflp_symp_transp reflp_def symp_def transp_def |
22 by (auto intro: list_eq.intros list_eq_refl) |
22 by (auto intro: list_eq.intros list_eq_refl) |
23 |
23 |
24 quotient_type fset = "'a list" / "list_eq" |
24 quotient_type |
|
25 'a fset = "'a list" / "list_eq" |
25 by (rule equivp_list_eq) |
26 by (rule equivp_list_eq) |
26 |
27 |
27 quotient_definition |
28 quotient_definition |
28 "fempty :: 'a fset" ("{||}") |
29 "fempty :: 'a fset" ("{||}") |
29 as |
30 as |