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
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