| changeset 43815 | 4f6e2965d821 |
| parent 37765 | 26bdfb7b680b |
| child 49190 | e1e1d427747d |
--- a/src/HOL/Library/Option_ord.thy Wed Jul 13 19:43:12 2011 +0200 +++ b/src/HOL/Library/Option_ord.thy Wed Jul 13 23:41:13 2011 +0200 @@ -58,7 +58,7 @@ instance option :: (linorder) linorder proof qed (auto simp add: less_eq_option_def less_option_def split: option.splits) -instantiation option :: (preorder) bot +instantiation option :: (order) bot begin definition "bot = None"