equal
deleted
inserted
replaced
20 sorry |
20 sorry |
21 |
21 |
22 quotient fset = "'a list" / "list_eq" |
22 quotient fset = "'a list" / "list_eq" |
23 by (rule list_eq_equivp) |
23 by (rule list_eq_equivp) |
24 |
24 |
25 lemma not_nil_equiv_cons: "\<not>[] \<approx> a # A" sorry |
25 lemma not_nil_equiv_cons: "\<not>[] \<approx> a # A" |
|
26 unfolding list_eq_def by auto |
26 |
27 |
27 (* The 2 lemmas below are different from the ones in QuotList *) |
28 (* The 2 lemmas below are different from the ones in QuotList *) |
28 lemma nil_rsp[quot_respect]: |
29 lemma nil_rsp[quot_respect]: |
29 shows "[] \<approx> []" |
30 shows "[] \<approx> []" |
30 by (rule list_eq_reflp) |
31 by (rule list_eq_reflp) |