--- a/src/HOL/Library/Product_Lexorder.thy Wed Jul 24 17:15:59 2013 +0200
+++ b/src/HOL/Library/Product_Lexorder.thy Thu Jul 25 08:57:16 2013 +0200
@@ -65,22 +65,26 @@
definition
"bot = (bot, bot)"
-instance
- by default (auto simp add: bot_prod_def)
+instance ..
end
+instance prod :: (order_bot, order_bot) order_bot
+ by default (auto simp add: bot_prod_def)
+
instantiation prod :: (top, top) top
begin
definition
"top = (top, top)"
-instance
- by default (auto simp add: top_prod_def)
+instance ..
end
+instance prod :: (order_top, order_top) order_top
+ by default (auto simp add: top_prod_def)
+
instance prod :: (wellorder, wellorder) wellorder
proof
fix P :: "'a \<times> 'b \<Rightarrow> bool" and z :: "'a \<times> 'b"