Re: [isabelle] Sledge and 0; green & blue; ATPs lovin' quantifiers

This has occurred to me. That the reason the ATPs may not be able to prove the theorem with the free variable, rather than the universally quantified variable, is because all my previous theorems are done with universal quantifiers rather than free variables.

To find out if that's true, I would need to change all the theorems so that they use free variables.


This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.