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

Alexander Krauss krauss at in.tum.de
Wed Nov 11 23:08:12 CET 2009

Hi Steven,

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

I hope there will be soon. Until that, please consider it as vapourware :-)


More information about the isabelle-dev mailing list