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

diff -r be337ec31268 -r 19c01bd7f6ae src/HOL/Lattices.thy
--- a/src/HOL/Lattices.thy	Wed Sep 30 17:09:06 2009 +0200
+++ b/src/HOL/Lattices.thy	Wed Sep 30 17:16:01 2009 +0200
@@ -535,6 +535,18 @@
 
 end
 
+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)
+
 
 subsection {* Fun as lattice *}