Re: [isabelle] Illegal schematic goal statement



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.