equal
deleted
inserted
replaced
45 fix x y :: parity show "(x < y) = (x \<le> y \<and> \<not> y \<le> x)" by(rule less_parity_def) |
45 fix x y :: parity show "(x < y) = (x \<le> y \<and> \<not> y \<le> x)" by(rule less_parity_def) |
46 qed |
46 qed |
47 |
47 |
48 end |
48 end |
49 |
49 |
50 text{* Instantiation of class @{class semilattice} with type @{typ parity}: *} |
50 text{* Instantiation of class @{class semilattice_sup_top} with type @{typ parity}: *} |
51 |
51 |
52 instantiation parity :: semilattice |
52 instantiation parity :: semilattice_sup_top |
53 begin |
53 begin |
54 |
54 |
55 definition sup_parity where |
55 definition sup_parity where |
56 "x \<squnion> y = (if x = y then x else Either)" |
56 "x \<squnion> y = (if x = y then x else Either)" |
57 |
57 |