Re: [isabelle] dest versus elim?


chapter 5 of the tutorial (rules of the game) is exactly the right thing
to read (the whole chapter), in particluar 5.2..5.4 may answer your


On Do, 2016-03-10 at 12:54 +0100, Freek Wiedijk wrote:
> Dear all,
> 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!
> Freek

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