equal
deleted
inserted
replaced
189 lemma ex1tst: "Bexeq (op \<approx>) (\<lambda>x :: nat \<times> nat. x \<approx> x)" |
189 lemma ex1tst: "Bexeq (op \<approx>) (\<lambda>x :: nat \<times> nat. x \<approx> x)" |
190 sorry |
190 sorry |
191 |
191 |
192 lemma ex1tst': "\<exists>! (x :: my_int). x = x" |
192 lemma ex1tst': "\<exists>! (x :: my_int). x = x" |
193 apply(lifting ex1tst) |
193 apply(lifting ex1tst) |
194 |
|
195 apply injection |
|
196 apply (rule quot_respect(9)) |
|
197 apply (rule Quotient_my_int) |
|
198 done |
194 done |
199 |
195 |
200 lemma ho_tst: "foldl my_plus x [] = x" |
196 lemma ho_tst: "foldl my_plus x [] = x" |
201 apply simp |
197 apply simp |
202 done |
198 done |