# HG changeset patch
# User haftmann
# Date 1394697368 -3600
# Node ID e52fc7c37ed305c484a67e2172da1a74c934b5e1
# Parent  c6d4425f1fdcdfdbef5aab8756eb0b1d3f15b827
dropped redundant theorems

diff -r c6d4425f1fdc -r e52fc7c37ed3 NEWS
--- a/NEWS	Thu Mar 13 08:56:08 2014 +0100
+++ b/NEWS	Thu Mar 13 08:56:08 2014 +0100
@@ -104,6 +104,8 @@
   can be restored like this:  declare/using [[simp_legacy_precond]]
   This configuration option will disappear again in the future.
 
+* Dropped facts INF_comp, SUP_comp.  INCOMPATIBILITY.
+
 * HOL-Word:
   * Abandoned fact collection "word_arith_alts", which is a
   duplicate of "word_arith_wis".
diff -r c6d4425f1fdc -r e52fc7c37ed3 src/HOL/Complete_Lattices.thy
--- a/src/HOL/Complete_Lattices.thy	Thu Mar 13 08:56:08 2014 +0100
+++ b/src/HOL/Complete_Lattices.thy	Thu Mar 13 08:56:08 2014 +0100
@@ -20,10 +20,6 @@
 definition INFI :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
   INF_def: "INFI A f = \<Sqinter>(f ` A)"
 
-lemma INF_comp: -- {* FIXME drop *}
-  "INFI A (g \<circ> f) = INFI (f ` A) g"
-  by (simp add: INF_def image_comp)
-
 lemma INF_image [simp]: "INFI (f`A) g = INFI A (\<lambda>x. g (f x))"
   by (simp add: INF_def image_image)
 
@@ -39,10 +35,6 @@
 definition SUPR :: "'b set \<Rightarrow> ('b \<Rightarrow> 'a) \<Rightarrow> 'a" where
   SUP_def: "SUPR A f = \<Squnion>(f ` A)"
 
-lemma SUP_comp: -- {* FIXME drop *}
-  "SUPR A (g \<circ> f) = SUPR (f ` A) g"
-  by (simp add: SUP_def image_comp)
-
 lemma SUP_image [simp]: "SUPR (f`A) g = SUPR A (%x. g (f x))"
   by (simp add: SUP_def image_image)