[isabelle] dest versus elim?
My apologies for a newbie question.
I am trying to understand the relationship between "dest"
and "elim". From
I got the impression that "elim" is a generalisation of
"dest". But in the Tutorial (reference from that message)
I read in 5.7 that "erule" unifies Q with the subgoal,
while "drule" does not. So that seems to imply that "erule"
might fail where "drule" does not?
In the example files for Concrete Semantics, I see lemmas
(for example "SkipE") that are proved with "[elim]", but
where I think that you do not only want to use them when
their conclusion unifies with the goal?
A pointer to a relevant book/manual is all I need. And if
this is too trivial, do not bother the list with this!
This archive was generated by a fusion of
Pipermail (Mailman edition) and