Quot/Examples/FSet2.thy
changeset 766 df053507edba
parent 705 f51c6069cd17
child 767 37285ec4387d
equal deleted inserted replaced
765:d0250d01782c 766:df053507edba
    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 fset = "'a list" / "list_eq"
    24 quotient_type fset = "'a list" / "list_eq"
    25   by (rule equivp_list_eq)
    25   by (rule equivp_list_eq)
    26 
    26 
    27 quotient_def
    27 quotient_def
    28   "fempty :: 'a fset" ("{||}")
    28   "fempty :: 'a fset" ("{||}")
    29 as
    29 as