Re: [isabelle] strange error message



> the name ("x" and "y" in your examples) refers to variables of the fact
> you are using, which is "allE", not to names inside the current goal.
> 
> allE: âx. ?P x â (?P ?x â ?R) â ?R
> 
> As you can see, there is an "x" in "allE", but not "y", hence the error
> message.

To clarify further, the "x" Christian is talking about is the so-called schematic variable "?x" occurring in the second assumption, not the bound "x" occurring in the first one. Although the variable's official name is "?x", there is no need to specify the question mark when instantiating it.

Jasmin





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