Re: [isabelle] download all the entries for all the packages needed


you can either download the whole AFP as Tobias suggested, or you can use the "Depends On" column in the entry description on

In this case it says that you'll need the entries Refine_Monadic and Collections, and Collections needs Binomial-Heaps and Finger-Trees.

I think you have discovered the deepest dependency tree in the whole AFP with this entry -- usually there are 0 or 1 steps only.


On 18/10/2012, at 11:50 PM, li yongjian <lyj238 at> wrote:

> Hi, Isabelle experts:
>  I have downloaded the theory package shortest_path from AFP, but
> when I run the proof
>  script dijkstra.thy, it need the Refine_Monadic/Refine.thy, which
> in turn need another
>  theory package collection?
>  Can anyone tell me how to download all the entries for all the
> packages needed?
>  best

The information in this e-mail may be confidential and subject to legal professional privilege and/or copyright. National ICT Australia Limited accepts no liability for any damage caused by this email or its attachments.

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