Re: [isabelle] More problems with induction



On Tue, 23 Oct 2007, Peter Lammich wrote:

> Is there any documentation/tutorial information on how the induct method 
> works and what all the parameters mean (e.g. arbitrary). The 
> Isabelle/HOL Tutorial only covers induct_tac.

See the isar-ref manual.  Some common patterns are given in 
HOL/Induct/Common_Patterns.thy


	Makarius






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