src/HOL/Library/Quickcheck_Types.thy
changeset 43815 4f6e2965d821
parent 40654 a716071ec306
child 44890 22f665a2e91c
     1.1 --- a/src/HOL/Library/Quickcheck_Types.thy	Wed Jul 13 19:43:12 2011 +0200
     1.2 +++ b/src/HOL/Library/Quickcheck_Types.thy	Wed Jul 13 23:41:13 2011 +0200
     1.3 @@ -108,7 +108,7 @@
     1.4  instance bot :: (linorder) linorder proof
     1.5  qed (auto simp add: less_eq_bot_def less_bot_def split: bot.splits)
     1.6  
     1.7 -instantiation bot :: (preorder) bot
     1.8 +instantiation bot :: (order) bot
     1.9  begin
    1.10  
    1.11  definition "bot = Bot"
    1.12 @@ -208,7 +208,7 @@
    1.13  instance top :: (linorder) linorder proof
    1.14  qed (auto simp add: less_eq_top_def less_top_def split: top.splits)
    1.15  
    1.16 -instantiation top :: (preorder) top
    1.17 +instantiation top :: (order) top
    1.18  begin
    1.19  
    1.20  definition "top = Top"