[isabelle-dev] (Re-)introducing set as a type constructor rather than as mere abbreviation

Lawrence Paulson lp15 at cam.ac.uk
Wed Aug 24 15:36:04 CEST 2011

I've just been trying to get the proofs working, not to simplify them or even to understand them. Incidentally, let there be no illusions about people accidentally stumbling into a mixture of sets and predicates. Some of these theories were clearly designed from the ground upwards on the premise that sets and predicates were the same thing.

On 23 Aug 2011, at 22:24, Alexander Krauss wrote:

> Shouldn't one remove quite a bit of duplication first? The classes distributive_complete_lattice and complete_boolean_algebra are now part of HOL (the former as complete_distrib_lattice) (see the FIXME). The set instances for those should be in/go into Florian's HOL repository as well...
> (but maybe you already did this???)

More information about the isabelle-dev mailing list