Re: [isabelle] Blast behaves strangely with free schematic variables
On Sunday 19 February 2006 11:36, Peter wrote:
> lemma bug: "?A & ?B & ?XYZZY --> ?XYZZY" by blast
> lemma bug: ?A & ?B &  \<in> lists ?Aa -->  \<in> lists ?Aa
as Larry already wrote, schematic variables can be replaced by any well-formed
term. If you find the above behavior surprising, maybe you just want to
input your lemma using free variables (without the question marks), e.g.
lemma foo: "A & B & XYZZY --> XYZZY" by blast
NB: Isabelle issues a warning "Goal statement contains unbound schematic
variable(s)" for the "bug" lemma.
This archive was generated by a fusion of
Pipermail (Mailman edition) and