[isabelle] strange error message
I am a french beginner in Isabelle.
I write this very short theory with jEdit
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