# HG changeset patch
# User haftmann
# Date 1254324180 -7200
# Node ID faf347097852985770103d862aeb46c3ac9b0cb1
# Parent  19c01bd7f6ae87947fddd2a5b48aa9cd6e0b768e
moved lemmas about sup on bool to Lattices.thy

diff -r 19c01bd7f6ae -r faf347097852 src/HOL/Predicate.thy
--- a/src/HOL/Predicate.thy	Wed Sep 30 17:16:01 2009 +0200
+++ b/src/HOL/Predicate.thy	Wed Sep 30 17:23:00 2009 +0200
@@ -19,21 +19,6 @@
 
 subsection {* Predicates as (complete) lattices *}
 
-subsubsection {* @{const sup} on @{typ bool} *}
-
-lemma sup_boolI1:
-  "P \<Longrightarrow> P \<squnion> Q"
-  by (simp add: sup_bool_eq)
-
-lemma sup_boolI2:
-  "Q \<Longrightarrow> P \<squnion> Q"
-  by (simp add: sup_bool_eq)
-
-lemma sup_boolE:
-  "P \<squnion> Q \<Longrightarrow> (P \<Longrightarrow> R) \<Longrightarrow> (Q \<Longrightarrow> R) \<Longrightarrow> R"
-  by (auto simp add: sup_bool_eq)
-
-
 subsubsection {* Equality *}
 
 lemma pred_equals_eq: "((\<lambda>x. x \<in> R) = (\<lambda>x. x \<in> S)) = (R = S)"