[isabelle-dev] Must the AFP be used as a component? (was: Reasons mira crashes)

Gerwin Klein Gerwin.Klein at nicta.com.au
Fri Dec 14 11:18:48 CET 2012

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 ../



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.

More information about the isabelle-dev mailing list