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

Alex





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