src/HOL/Main.thy
changeset 44860 56101fa00193
parent 44324 d972b91ed09d
child 44918 6a80fbc4e72c
     1.1 --- a/src/HOL/Main.thy	Sat Sep 10 00:44:25 2011 +0200
     1.2 +++ b/src/HOL/Main.thy	Sat Sep 10 10:29:24 2011 +0200
     1.3 @@ -21,7 +21,7 @@
     1.4    "Sup A \<longleftrightarrow> (\<exists>x\<in>A. x)"
     1.5    by auto
     1.6  
     1.7 -declare Complete_Lattice.Inf_bool_def [simp del]
     1.8 -declare Complete_Lattice.Sup_bool_def [simp del]
     1.9 +declare Complete_Lattices.Inf_bool_def [simp del]
    1.10 +declare Complete_Lattices.Sup_bool_def [simp del]
    1.11  
    1.12  end