Re: [isabelle] dest versus elim?



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!

Freek




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