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 <nosch...@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-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
