equal
deleted
inserted
replaced
30 |
30 |
31 definition |
31 definition |
32 "(sup \<Colon> nibble \<Rightarrow> _) = max" |
32 "(sup \<Colon> nibble \<Rightarrow> _) = max" |
33 |
33 |
34 instance proof |
34 instance proof |
35 qed (auto simp add: inf_nibble_def sup_nibble_def min_max.sup_inf_distrib1) |
35 qed (auto simp add: inf_nibble_def sup_nibble_def max_min_distrib2) |
36 |
36 |
37 end |
37 end |
38 |
38 |
39 instantiation char :: linorder |
39 instantiation char :: linorder |
40 begin |
40 begin |
88 |
88 |
89 definition |
89 definition |
90 "(sup \<Colon> char \<Rightarrow> _) = max" |
90 "(sup \<Colon> char \<Rightarrow> _) = max" |
91 |
91 |
92 instance proof |
92 instance proof |
93 qed (auto simp add: inf_char_def sup_char_def min_max.sup_inf_distrib1) |
93 qed (auto simp add: inf_char_def sup_char_def max_min_distrib2) |
94 |
94 |
95 end |
95 end |
96 |
96 |
97 instantiation String.literal :: linorder |
97 instantiation String.literal :: linorder |
98 begin |
98 begin |