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