changeset 62343 24106dc44def
parent 62053 1c8252d07e32
child 63561 fba08009ff3e
--- a/src/HOL/Library/Product_Order.thy	Wed Feb 17 21:51:55 2016 +0100
+++ b/src/HOL/Library/Product_Order.thy	Wed Feb 17 21:51:56 2016 +0100
@@ -179,7 +179,6 @@
 instance prod :: (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)+
 instance prod :: (complete_lattice, complete_lattice) complete_lattice
@@ -211,10 +210,10 @@
   using snd_Inf [of "f ` A", symmetric] by (simp add: comp_def)
 lemma SUP_Pair: "(SUP x:A. (f x, g x)) = (SUP x:A. f x, SUP x:A. g x)"
-  unfolding SUP_def Sup_prod_def by (simp add: comp_def)
+  unfolding Sup_prod_def by (simp add: comp_def)
 lemma INF_Pair: "(INF x:A. (f x, g x)) = (INF x:A. f x, INF x:A. g x)"
-  unfolding INF_def Inf_prod_def by (simp add: comp_def)
+  unfolding Inf_prod_def by (simp add: comp_def)
 text \<open>Alternative formulations for set infima and suprema over the product
@@ -222,11 +221,11 @@
 lemma INF_prod_alt_def:
   "INFIMUM A f = (INFIMUM A (fst o f), INFIMUM A (snd o f))"
-  unfolding INF_def Inf_prod_def by simp
+  unfolding Inf_prod_def by simp
 lemma SUP_prod_alt_def:
   "SUPREMUM A f = (SUPREMUM A (fst o f), SUPREMUM A (snd o f))"
-  unfolding SUP_def Sup_prod_def by simp
+  unfolding Sup_prod_def by simp
 subsection \<open>Complete distributive lattices\<close>