Re: [isabelle] using AFP



Isabelle opens Complete_Lattice_Prop.thy, and this file does not have
errors. Only the test file has the error. I tried some other random
theory from AFP, and I get exactly the same behavior.

In the theory panel the the Test file is marked with red. When
opening the test file Isabelle asks to open the files on which Test dependents,
However after opening them it asks again about opening one of these
files.

Viorel


On 6/16/2014 7:07 PM, Lars Noschinski wrote:
On 16.06.2014 15:58, Viorel Preoteasa wrote:
This is in Isabelle/jEdit. I tried to save the file. I also
tried to close Isabelle and open it again, but I get the
same error.
Does I/jEdit open the Complete_Lattice_Prop.thy file? If yes, is there
any error in this file (have a look at the theories panel)?

   -- Lars






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