| changeset 69815 | 56d5bb8c102e |
| parent 69597 | ff784d5a5bfb |
| 69814:5929b172c6fe | 69815:56d5bb8c102e |
|---|---|
277 then show "f \<cong> g" by (rule equiv_funI) |
277 then show "f \<cong> g" by (rule equiv_funI) |
278 qed |
278 qed |
279 qed |
279 qed |
280 qed |
280 qed |
281 |
281 |
282 declare fun_order.antisym [intro?] |
282 declare fun_order.equiv_antisym [intro?] |
283 |
283 |
284 |
284 |
285 subsection \<open>Simple examples\<close> |
285 subsection \<open>Simple examples\<close> |
286 |
286 |
287 text \<open> |
287 text \<open> |