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