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

Steven Obua obua at in.tum.de
Wed Nov 11 22:54:14 CET 2009

> 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?



PS: For those of you who a) speak German b) play Skat c) have an  
iPhone / iPod touch:

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20091111/b168d2c1/attachment.html>

More information about the isabelle-dev mailing list