# Re: [isabelle] Free variables aren't quantified, it's that simple (by all appearances)

It sort of escaped my notice that although I have
theorem --"(4)"
"(!C.!D.(C | D --> C)) --> (A | B --> A)"
by auto

`I also have anything else I want to prove, for the simple fact that the
``hypothesis is always false.
`
theorem --"(4a)"
"(!C.!D.(C | D --> C)) --> P a"
by auto

`This could be material for my book, "How to Learn Basic Logic with
``Isabelle", or with the type of title I always hate, "Logic for Dummies
``with Isabelle2012".
`http://www.amazon.com/Logic-For-Dummies-Mark-Zegarelli/dp/0471799416

`It still appears that free variables aren't quantified, although my
``reasoning might be warped. It may not be warped. If I just know what's
``true, then I can sometimes straighten out my reasoning.
`

`This is my first use of Isabelle as a tool to confirm some basic logic.
``No one else is going to take any substantial time to clarify and remind
``me of the basics that I mostly understand. There's nothing wrong with that.
`
Regards,
GB

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