1.1 --- a/src/HOL/Library/Product_Order.thy	Wed Jul 24 17:15:59 2013 +0200
     1.2 +++ b/src/HOL/Library/Product_Order.thy	Thu Jul 25 08:57:16 2013 +0200
     1.3 @@ -108,6 +108,10 @@
     1.4  definition
     1.5    "top = (top, top)"
     1.6  
     1.7 +instance ..
     1.8 +
     1.9 +end
    1.10 +
    1.11  lemma fst_top [simp]: "fst top = top"
    1.12    unfolding top_prod_def by simp
    1.13  
    1.14 @@ -117,17 +121,19 @@
    1.15  lemma Pair_top_top: "(top, top) = top"
    1.16    unfolding top_prod_def by simp
    1.17  
    1.18 -instance
    1.19 +instance prod :: (order_top, order_top) order_top
    1.20    by default (auto simp add: top_prod_def)
    1.21  
    1.22 -end
    1.23 -
    1.24  instantiation prod :: (bot, bot) bot
    1.25  begin
    1.26  
    1.27  definition
    1.28    "bot = (bot, bot)"
    1.29  
    1.30 +instance ..
    1.31 +
    1.32 +end
    1.33 +
    1.34  lemma fst_bot [simp]: "fst bot = bot"
    1.35    unfolding bot_prod_def by simp
    1.36  
    1.37 @@ -137,11 +143,9 @@
    1.38  lemma Pair_bot_bot: "(bot, bot) = bot"
    1.39    unfolding bot_prod_def by simp
    1.40  
    1.41 -instance
    1.42 +instance prod :: (order_bot, order_bot) order_bot
    1.43    by default (auto simp add: bot_prod_def)
    1.44  
    1.45 -end
    1.46 -
    1.47  instance prod :: (bounded_lattice, bounded_lattice) bounded_lattice ..
    1.48  
    1.49  instance prod :: (boolean_algebra, boolean_algebra) boolean_algebra
    1.50 @@ -161,7 +165,7 @@
    1.51  
    1.52  instance
    1.53    by default (simp_all add: less_eq_prod_def Inf_prod_def Sup_prod_def
    1.54 -    INF_lower SUP_upper le_INF_iff SUP_le_iff)
    1.55 +    INF_lower SUP_upper le_INF_iff SUP_le_iff bot_prod_def top_prod_def)
    1.56  
    1.57  end
    1.58