Re: [isabelle] Illegal schematic goal statement

Right, that's what I was trying to get at.


On 01/04/15 10:43, Lars Noschinski wrote:
On 01.04.2015 09:36, Manuel Eberl wrote:
Why of course you can: "?x + ?x".
However, you cannot search for a lemma which contains both "odd x" and
"even x" for the same x,
as in the query "odd ?x" "even ?x" both ?x are allowed to be different.

   -- Lars

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