Re: [isabelle] Question about drule_tac

and want apply drule_tac as follows:
apply(drule_tac sigma = "% y. if y = 1 then 2 else (if y = 2 then 1 else y)"
       in allE)

in order to instantiate the universally quantified variable sigma with the
lambda expression %y ...., but get the error:

*** No such variable in theorem: ?sigma
*** At command "apply".

The name "sigma" in (drule_tac sigma = ... in allE) refers to the variable name in the theorem to be instantiated, that is, allE. So it must be "x" instead of "sigma".

Hope this helps


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