Re: [isabelle] strange error message



Dear Michel,

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
message.

hope this helps

chris

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
> 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 ?
> 




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