src/HOL/Complete_Lattice.thy
changeset 43818 fcc5d3ffb6f5
parent 43817 d53350bc65a4
child 43831 e323be6b02a5
     1.1 --- a/src/HOL/Complete_Lattice.thy	Thu Jul 14 00:16:41 2011 +0200
     1.2 +++ b/src/HOL/Complete_Lattice.thy	Thu Jul 14 00:20:43 2011 +0200
     1.3 @@ -6,14 +6,6 @@
     1.4  imports Set
     1.5  begin
     1.6  
     1.7 -lemma ball_conj_distrib:
     1.8 -  "(\<forall>x\<in>A. P x \<and> Q x) \<longleftrightarrow> ((\<forall>x\<in>A. P x) \<and> (\<forall>x\<in>A. Q x))"
     1.9 -  by blast
    1.10 -
    1.11 -lemma bex_disj_distrib:
    1.12 -  "(\<exists>x\<in>A. P x \<or> Q x) \<longleftrightarrow> ((\<exists>x\<in>A. P x) \<or> (\<exists>x\<in>A. Q x))"
    1.13 -  by blast
    1.14 -
    1.15  notation
    1.16    less_eq (infix "\<sqsubseteq>" 50) and
    1.17    less (infix "\<sqsubset>" 50) and