# HG changeset patch
# User haftmann
# Date 1398511546 -7200
# Node ID 2b3710a4fa94f0d658c2e254b9cbb6532d94474f
# Parent  5ebaa364d8ab2aeb9711292524b91152ccc8b98d
subsumed by existing default simp rules for functions and booleans

diff -r 5ebaa364d8ab -r 2b3710a4fa94 src/HOL/Complete_Lattices.thy
--- a/src/HOL/Complete_Lattices.thy	Sat Apr 26 13:25:45 2014 +0200
+++ b/src/HOL/Complete_Lattices.thy	Sat Apr 26 13:25:46 2014 +0200
@@ -758,12 +758,6 @@
 
 subsection {* Complete lattice on unary and binary predicates *}
 
-lemma INF1_iff: "(\<Sqinter>x\<in>A. B x) b = (\<forall>x\<in>A. B x b)"
-  by simp
-
-lemma INF2_iff: "(\<Sqinter>x\<in>A. B x) b c = (\<forall>x\<in>A. B x b c)"
-  by simp
-
 lemma INF1_I: "(\<And>x. x \<in> A \<Longrightarrow> B x b) \<Longrightarrow> (\<Sqinter>x\<in>A. B x) b"
   by auto
 
@@ -782,12 +776,6 @@
 lemma INF2_E: "(\<Sqinter>x\<in>A. B x) b c \<Longrightarrow> (B a b c \<Longrightarrow> R) \<Longrightarrow> (a \<notin> A \<Longrightarrow> R) \<Longrightarrow> R"
   by auto
 
-lemma SUP1_iff: "(\<Squnion>x\<in>A. B x) b = (\<exists>x\<in>A. B x b)"
-  by simp
-
-lemma SUP2_iff: "(\<Squnion>x\<in>A. B x) b c = (\<exists>x\<in>A. B x b c)"
-  by simp
-
 lemma SUP1_I: "a \<in> A \<Longrightarrow> B a b \<Longrightarrow> (\<Squnion>x\<in>A. B x) b"
   by auto