equal
deleted
inserted
replaced
405 |
405 |
406 lemma "All (\<lambda> (x :: 'a fset, y, z). x = y \<and> y = z)" |
406 lemma "All (\<lambda> (x :: 'a fset, y, z). x = y \<and> y = z)" |
407 apply (lifting test4) |
407 apply (lifting test4) |
408 sorry |
408 sorry |
409 |
409 |
410 lemma test5: "\<forall> (x :: 'a list \<Rightarrow> 'a list, y, z) \<in> Respects( |
410 lemma test5: "\<forall> (x :: 'a list \<Rightarrow> 'a list, y) \<in> Respects( |
411 prod_rel (op \<approx> ===> op \<approx>) (prod_rel (op \<approx> ===> op \<approx>) (op \<approx> ===> op \<approx>)) |
411 prod_rel (op \<approx> ===> op \<approx>) (op \<approx> ===> op \<approx>) |
412 ). x = y \<and> y = z" |
412 ). x = y" |
413 sorry |
413 sorry |
414 |
414 |
415 lemma "All (\<lambda> (x :: 'a fset \<Rightarrow> 'a fset, y, z). x = y \<and> y = z)" |
415 lemma "All (\<lambda> (x :: 'a fset \<Rightarrow> 'a fset, y). x = y)" |
416 apply (lifting test5) |
416 apply (lifting test5) |
417 sorry |
417 sorry |
418 |
418 |
419 |
419 |
420 end |
420 end |