Re: [isabelle] Difficulties with Isar proofs and fix



On Tue, 26 Feb 2008, Denis Bueno wrote:

>  It requires the LList2 library (lazy, infinite lists) available at 
>  http://afp.sourceforge.net/entries/Lazy-Lists-II.shtml.

Just note that LList is based on the old HOL/ex/LList; there is also a 
renovated and Isar-ized version in HOL/Library/Coinductive_List. In 
particular, the proof method "coinduct" is used here for well-structured 
coinduction proofs.  Ideally AFP's LList2 would be converted to make use 
of the newer Coinductive_List at some point.


	Makarius






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