[isabelle] dest versus elim?



Dear all,

My apologies for a newbie question.

I am trying to understand the relationship between "dest"
and "elim".  From

<https://lists.cam.ac.uk/pipermail/cl-isabelle-users/2008-March/msg00077.html>

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!

Freek




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