--- 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 *}