src/HOL/Complete_Lattice.thy
changeset 43866 8a50dc70cbff
parent 43865 db18f4d0cc7d
child 43867 771014555553
     1.1 --- a/src/HOL/Complete_Lattice.thy	Sun Jul 17 15:15:58 2011 +0200
     1.2 +++ b/src/HOL/Complete_Lattice.thy	Sun Jul 17 19:48:02 2011 +0200
     1.3 @@ -564,10 +564,6 @@
     1.4    "(\<Sqinter>x\<in>UNIV. f x) = \<Sqinter>range f"
     1.5    by (simp add: INFI_def)
     1.6  
     1.7 -lemma UNIV_bool [no_atp]: -- "FIXME move"
     1.8 -  "UNIV = {False, True}"
     1.9 -  by auto
    1.10 -
    1.11  lemma (in complete_lattice) INF_bool_eq:
    1.12    "(\<Sqinter>b. A b) = A True \<sqinter> A False"
    1.13    by (simp add: UNIV_bool INF_empty INF_insert inf_commute)