Re: [isabelle] Using Isar on Induction



On Sun, 29 Apr 2012 06:56:06 +0200, Brian Huffman wrote:

> Instead of "by (simp only: dd) simp", try "unfolding dd by simp".
> 
> The "unfolding" command will do rewriting on the goal and in the chained
> facts, but unlike "apply simp" it leaves the chained facts as chained
> facts.

This works great. Thank you.  Is there a place where I can read up on all 
of these?  Right now I am just going through the many tutorials.

-- 
Aaron W. Hsu | arcfide at sacrideo.us | http://www.sacrideo.us
Programming is just another word for the lost art of thinking.






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