[isabelle] x is a special variable
I am an french beginner in Isabelle. I prove (as an exercise) the
lemma "â y. P y â P (f a)"
apply (erule_tac x="f a" in allE)
But why am I obliged to use x in instantiating the quantifier (x = "f a").
If I use y = "f a" to instantiate the quantifier, I have a message "no
such variable in theorem".
email : michel.levy at imag.fr
This archive was generated by a fusion of
Pipermail (Mailman edition) and