| changeset 44026 | d5e28a49e16e |
| parent 44007 | b5e7594061ce |
| child 44033 | bc45393f497b |
--- a/src/HOL/Predicate.thy Wed Aug 03 23:21:52 2011 +0200 +++ b/src/HOL/Predicate.thy Wed Aug 03 23:21:53 2011 +0200 @@ -431,7 +431,7 @@ "x \<in> (op =) y \<longleftrightarrow> x = y" by (auto simp add: mem_def) -instantiation pred :: (type) "{complete_lattice, boolean_algebra}" +instantiation pred :: (type) complete_boolean_algebra begin definition