[isabelle-dev] Must the AFP be used as a component?

[Christian Sternagel]

Dear all,

I think I already used the $AFP in my original submission. The reason 
was that having such a variable seemed more robust to me than just 
having a relative "../" (so a user could put the entry anywhere he 
wants). Sorry for the confusion.

cheers

chris

On 12/14/2012 07:18 PM, Gerwin Klein wrote:
> On 14/12/2012, at 6:55 PM, Lars Noschinski <noschinl at in.tum.de> wrote:
>> The reason is that Open_Induction/ROOT (and also Open_Induction/Open_Induction.thy) relies on $AFP being set, which is only the case if AFP is registered as a component (which is not the case for Mira).
>>
>> @Gerwin: Since you made the ROOT file, what was the intention of using $AFP instead of ../ used in all other theories?
>
> I think I was just experimenting with the new build system. Not a successful experiment, it seems. I'll change it to the usual ../
>
> 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.
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>