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 |
Programming is just another word for the lost art of thinking.

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