[isabelle] Blast behaves strangely with free schematic variables
I downloaded Isabelle2005 just now following the installation
and if I start my "ToyList.thy" file with
lemma bug: "?A & ?B & ?XYZZY \<longrightarrow> ?XYZZY" by blast
and go to the end and press control-c control-enter, I see this in the
lemma bug: ?A & ?B & gcd (?m, ?n) dvd ?n --> gcd (?m, ?n) dvd ?n
I had expected it to say:
lemma bug: ?A & ?B & ?XYZZY --> ?XYZZY
I was surprised by the intruction of the "gcd" operator. If I change
"blast" to "auto", I do get the output I expected.
Tim Freeman http://www.fungible.com tim at fungible.com
Pass it on: The Integral Fast Reactor can provide safe, clean
energy. Politically motivated misrepresentation stopped the research.
Check it out at: http://en.wikipedia.org/wiki/Integral_Fast_Reactor
This archive was generated by a fusion of
Pipermail (Mailman edition) and