equal
deleted
inserted
replaced
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 apply(auto intro: list_eq.intros list_eq_refl) |
22 apply(auto intro: list_eq.intros list_eq_refl) |
23 done |
23 done |
24 |
24 |
25 quotient_type |
25 quotient_type |
26 fset = "'a list" / "list_eq" |
26 'a fset = "'a list" / "list_eq" |
27 by (rule equivp_list_eq) |
27 by (rule equivp_list_eq) |
28 |
28 |
29 quotient_definition |
29 quotient_definition |
30 "EMPTY :: 'a fset" |
30 "EMPTY :: 'a fset" |
31 as |
31 as |
278 |
278 |
279 lemma "P (x :: 'a fset) ([] :: 'c list) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (e # t)) \<Longrightarrow> P x l" |
279 lemma "P (x :: 'a fset) ([] :: 'c list) \<Longrightarrow> (\<And>e t. P x t \<Longrightarrow> P x (e # t)) \<Longrightarrow> P x l" |
280 apply (lifting list_induct_part) |
280 apply (lifting list_induct_part) |
281 done |
281 done |
282 |
282 |
283 quotient_type fset2 = "'a list" / "list_eq" |
283 quotient_type 'a fset2 = "'a list" / "list_eq" |
284 by (rule equivp_list_eq) |
284 by (rule equivp_list_eq) |
285 |
285 |
286 quotient_definition |
286 quotient_definition |
287 "EMPTY2 :: 'a fset2" |
287 "EMPTY2 :: 'a fset2" |
288 as |
288 as |