Re: [isabelle] Coinduction



On Sun, 29 Jun 2008, Richard Warburton wrote:

> I was wondering if someone knew of any good examples of papers using 
> coinduction within Isabelle/HOL?  If there were available theory files 
> relating to such papers it would also be most helpful.

Here are some theories using coinduction:

  http://isabelle.in.tum.de/library/HOL/Library/Coinductive_List.html
  http://afp.sourceforge.net/entries/Lazy-Lists-II.shtml

The second is based on an old version of the first, namely 
http://isabelle.in.tum.de/library/HOL/Induct/LList.html


	Makarius





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