Re: [isabelle] [isabelle-dev] Some missing setup for function package in combination with Option-type

On Mon, 20 Feb 2012, Gerwin Klein wrote:

It may be enough to just put a download of the entire AFP wherever the users wants and add the appropriate line to the user components file.

This sounds good. The whole download is approx. 7MB compressed and 43MB uncompressed. This is tiny compared with the main Isabelle distribution.

By providing a suitable etc/settings its file-space can be easily injected into Isabelle via some $AFP variable. So imports can refer to theories like "$AFP/Foo/Bar".

Florian has basically already done the rest. The AFP is still of a size where we don't really need to disentangle separate entries.

This probably refers to

Florian has called it "rudimentary support for AFP as Isabelle component", but it looks fine to be. The remaining odditiy is that is unavailable for actual users: the official downloads of AFP only contain the content of the thys directory, without this etc/settings file.


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