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

[li yongjian]

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

[Tobias Nipkow]

The simplest solution is to download the whole AFP - it is not so big (yet).
Here is how you should install and use it: http://afp.sourceforge.net/using.shtml
There is no facility yet to pull in exactly the articles needed.

Best
Tobias

[Gerwin Klein]

Hi,

you can either download the whole AFP as Tobias suggested, or you can use the "Depends On" column in the entry description on
http://afp.sourceforge.net/entries/Dijkstra_Shortest_Path.shtml

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.

Cheers,
Gerwin

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.