Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
more specific instantiation
authorhaftmann
Wed, 03 Aug 2011 23:21:53 +0200
changeset 44026 d5e28a49e16e
parent 44025 ec2a7901217b
child 44027 d01b3f045111
more specific instantiation
src/HOL/Predicate.thy file | annotate | diff | comparison | revisions 
--- 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
isabelle