equal
deleted
inserted
replaced
253 quotient_type |
253 quotient_type |
254 'a abs_set = "(atom set \<times> 'a::pt)" / "alpha_abs_set" |
254 'a abs_set = "(atom set \<times> 'a::pt)" / "alpha_abs_set" |
255 and 'b abs_res = "(atom set \<times> 'b::pt)" / "alpha_abs_res" |
255 and 'b abs_res = "(atom set \<times> 'b::pt)" / "alpha_abs_res" |
256 and 'c abs_lst = "(atom list \<times> 'c::pt)" / "alpha_abs_lst" |
256 and 'c abs_lst = "(atom list \<times> 'c::pt)" / "alpha_abs_lst" |
257 apply(rule_tac [!] equivpI) |
257 apply(rule_tac [!] equivpI) |
258 unfolding reflp_def symp_def transp_def |
258 unfolding reflp_def refl_on_def symp_def sym_def transp_def trans_def |
259 by (auto intro: alphas_abs_sym alphas_abs_refl alphas_abs_trans simp only:) |
259 by (auto intro: alphas_abs_sym alphas_abs_refl alphas_abs_trans simp only:) |
260 |
260 |
261 quotient_definition |
261 quotient_definition |
262 Abs_set ("[_]set. _" [60, 60] 60) |
262 Abs_set ("[_]set. _" [60, 60] 60) |
263 where |
263 where |