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

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