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
hope this helps
On 10/12/2015 05:58 PM, michel levy wrote:
> I am a french beginner in Isabelle.
> I write this very short theory with jEdit
> theory all
> imports Main
> lemma "â x. P(w,x) â P(w,a)"
> apply(erule_tac x ="a" in allE)
> *Her**e I have the goal P(w,a) ==> P(w,a)*
> lemma "â y. P(w,y) â P(w,a)"
> apply(erule_tac y= "a" in allE)
> *Here I have the unexpected message No such variable in theorem : "?y"*
> Why this difference between these proofs ?
This archive was generated by a fusion of
Pipermail (Mailman edition) and