| changeset 910 | b91782991dc8 |
| parent 909 | 3e7a6ec549d1 |
| child 911 | 95ee248b3832 |
| 909:3e7a6ec549d1 | 910:b91782991dc8 |
|---|---|
193 apply(lifting ex1tst) |
193 apply(lifting ex1tst) |
194 |
194 |
195 apply injection |
195 apply injection |
196 apply (rule quot_respect(9)) |
196 apply (rule quot_respect(9)) |
197 apply (rule Quotient_my_int) |
197 apply (rule Quotient_my_int) |
198 |
|
199 apply(cleaning) |
|
200 apply (simp add: ex1_prs[OF Quotient_my_int]) |
|
201 done |
198 done |
202 |
199 |
203 lemma ho_tst: "foldl my_plus x [] = x" |
200 lemma ho_tst: "foldl my_plus x [] = x" |
204 apply simp |
201 apply simp |
205 done |
202 done |