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

[Lawrence Paulson]

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.
Larry

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???)