[isabelle] Re2: Antwort: Coinductive_List and LList/LFilter



Thank you for the explanation. I now plan to add a navigation aid for such 
long theories to my product Elbe .
Jens

>... these theories are not mine. Larry Paulson wrote LFilter and Stephan 
> Merz LList2. I merely ported them such that they now use 
> Coinductive_List from HOL/Library instead of Induct/LList. ...






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