Re: [isabelle] dest versus elim?

The book is intentionally ambiguous at this point. The fact that the inductive_cases command produces the rules in elimination format is merely a logical diversion. Hence I suppressed that discussion.


On 10/03/2016 14:40, Freek Wiedijk wrote:
Dear Peter,

thm SkipE
  â(SKIP, ?s) â ?t; ?t = ?s â ?Pâ â ?P

Oops!  From the book (on page 81) I had got the impression
that the theorem would be "(SKIP, s) => t ==> t = s".
(I hadn't actually tried it.)

I feel embarrassed now.  My apologies for the disturbance,
and thanks for all the help!


Attachment: smime.p7s
Description: S/MIME Cryptographic Signature

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