diff -r 8bcbf1c93119 -r 1c8252d07e32 src/HOL/Library/Product_Order.thy
--- a/src/HOL/Library/Product_Order.thy	Mon Jan 04 21:42:32 2016 +0100
+++ b/src/HOL/Library/Product_Order.thy	Mon Jan 04 21:49:06 2016 +0100
@@ -153,7 +153,7 @@
 instance prod :: (bounded_lattice, bounded_lattice) bounded_lattice ..
 
 instance prod :: (boolean_algebra, boolean_algebra) boolean_algebra
-  by standard (auto simp add: prod_eqI inf_compl_bot sup_compl_top diff_eq)
+  by standard (auto simp add: prod_eqI diff_eq)
 
 
 subsection \<open>Complete lattice operations\<close>
@@ -179,7 +179,8 @@
 instance prod :: (conditionally_complete_lattice, conditionally_complete_lattice)
     conditionally_complete_lattice
   by standard (force simp: less_eq_prod_def Inf_prod_def Sup_prod_def bdd_below_def bdd_above_def
-    INF_def SUP_def simp del: Inf_image_eq Sup_image_eq intro!: cInf_lower cSup_upper cInf_greatest cSup_least)+
+    INF_def SUP_def simp del: Inf_image_eq Sup_image_eq
+    intro!: cInf_lower cSup_upper cInf_greatest cSup_least)+
 
 instance prod :: (complete_lattice, complete_lattice) complete_lattice
   by standard (simp_all add: less_eq_prod_def Inf_prod_def Sup_prod_def