> > In the translation to ZF which Andy and I am developing, such > "strange proofs" actually caused some weird problems at some point.
This sounds interesting :-) Is there more information on this translation available? Best, Steven PS: For those of you who a) speak German b) play Skat c) have an iPhone / iPod touch: http://74.207.244.176/pubstatic/onlineskat -------------- next part -------------- An HTML attachment was scrubbed... URL: <https://mailmanbroy.informatik.tu-muenchen.de/pipermail/isabelle-dev/attachments/20091111/b168d2c1/attachment.htm>