[isabelle-dev] Isabelle/HOL axiom ext is redundant
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
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...
More information about the isabelle-dev