| changeset 5711 | 5a1cd4b4b20e |
| parent 5069 | 3ea049f7979d |
| 5710:30f4d3713cbe | 5711:5a1cd4b4b20e |
|---|---|
1 |
|
2 open LatMorph; |
|
3 |
1 |
4 |
2 |
5 (** monotone functions vs. "&&"- / "||"-semi-morphisms **) |
3 (** monotone functions vs. "&&"- / "||"-semi-morphisms **) |
6 |
4 |
7 Goalw [is_mono_def] "is_mono f = (ALL x y. f (x && y) [= f x && f y)"; |
5 Goalw [is_mono_def] "is_mono f = (ALL x y. f (x && y) [= f x && f y)"; |