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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
