Tobias Nipkow wrote: > Am 12/08/2011 11:27, schrieb Alexander Krauss: >> On 08/12/2011 07:51 AM, Tobias Nipkow wrote: >>> The benefits of getting rid of set were smaller than expected but quite >>> a bit of pain was and is inflicted. >> Do you know of any more pain, apart from what Florian already mentioned? > > I think he omitted to mention type classes. It comes up again and again > on the mailing list.
Really? In the thread http://thread.gmane.org/gmane.science.mathematics.logic.isabelle.user/260/ cited by Brian and Alex, Brendan was worried about the fact that one could no longer declare arities for sets. In my reply to his mail, I pointed out that arities for sets could usually be rephrased as arities for functions and booleans. I also asked him to give a concrete example for an arity where this was not possible, but I never got a reply, so I assume that this is not so much of a problem. Greetings, Stefan _______________________________________________ isabelle-dev mailing list [email protected] https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
