Re: [isabelle] [isabelle-dev] Some missing setup for function package in combination with Option-type
On 20/02/2012, at 10:53 PM, Makarius wrote:
> 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 http://afp.hg.sourceforge.net/hgweb/afp/afp/rev/5b970f669325
> 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.
Good point. That can easily be fixed.
This archive was generated by a fusion of
Pipermail (Mailman edition) and