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

[Alexander Krauss]

On 08/24/2011 03:36 PM, Lawrence Paulson wrote:
> 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.

I removed most of the duplication now in the main afp repos, which 
compiles again.

I'll have a more closer look at these theories in the next days.

Here are Larry's changesets, for reference:
https://www4.in.tum.de/~krauss/hg/afp-set-GraphMarking-paulson/

Alex