Re: [isabelle] using AFP
Curious. I’m assuming your theory file starts like this:
If I open this file by running “isabelle jedit” on the command line, I get a theory import dialog where it says it needs to load Complete_Lattice_Prop and another theory. After clicking Ok, it does so without errors.
What happens when you say
isabelle build -d /Applications/Isabelle2013-2.app/Isabelle/afp-2014-06-12/thys LatticeProperties
on the command line?
Does anything change when you run jedit like this?
isabelle jedit -d /Applications/Isabelle2013-2.app/Isabelle/afp-2014-06-12/thys
Also, just to make sure it’s picking up the right Isabelle version, what is the output of the following?
On 17.06.2014, at 4:04 am, Viorel Preoteasa <viorel.preoteasa at aalto.fi> wrote:
> 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
> 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
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and