equal
deleted
inserted
replaced
51 |
51 |
52 instantiation parity :: semilattice |
52 instantiation parity :: semilattice |
53 begin |
53 begin |
54 |
54 |
55 definition sup_parity where |
55 definition sup_parity where |
56 "x \<squnion> y = (if x \<le> y then y else if y \<le> x then x else Either)" |
56 "x \<squnion> y = (if x = y then x else Either)" |
57 |
57 |
58 definition top_parity where |
58 definition top_parity where |
59 "\<top> = Either" |
59 "\<top> = Either" |
60 |
60 |
61 text{* Now the instance proof. This time we take a lazy shortcut: we do not |
61 text{* Now the instance proof. This time we take a lazy shortcut: we do not |