[isabelle-dev] Isabelle/HOL axiom ext is redundant

[Steven Obua]

>
> 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://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20091111/b168d2c1/attachment.html>