On 06/16/2016 01:57 AM, Ramana Kumar wrote:
I expect it could be because the Boolean constants are spelled "T" and
"F" rather than "true" and "false" in the logic, so the latter are
being treated as free variables.
Thank you for your explanation. I am getting closer to getting my
definitio
I expect it could be because the Boolean constants are spelled "T" and "F"
rather than "true" and "false" in the logic, so the latter are being
treated as free variables.
On 16 June 2016 at 01:09, Heiko Becker wrote:
> Hello everyone,
>
> I am currently learning HOL-Light and therefore working t
