[isabelle] strange error message

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 ?

email : michel.levy at imag.fr

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