[isabelle] strange error message



I am a french beginner in Isabelle.
I write this very short theory with jEdit

theory all
imports Main
begin
  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)*
  oops

  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"*
  oops

Why this difference between these proofs ?

-- 
email : michel.levy at imag.fr
http://membres-liglab.imag.fr/michel.levy 




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