[isabelle] using AFP



I am trying to import some theory from AFP, but I get the following error:

Bad theory (file "/Applications/Isabelle2013-2.app/Isabelle/afp-2014-06-12/thys/LatticeProperties/Complete_Lattice_Prop.thy”)

I setup the path for afp in ~/.isabelle/Isabelle2013-2/etc/components:

/Applications/Isabelle2013-2.app/Isabelle/afp-2014-06-12/

and I installed AFP in /Applications/Isabelle2013-2.app/Isabelle/afp-2014-06-12/

I can access the path 
/Applications/Isabelle2013-2.app/Isabelle/afp-2014-06-12/thys/LatticeProperties/Complete_Lattice_Prop.thy

and Isabelle manages to load this file when loading the file which imports it.

Best regards,

Viorel Preoteasa


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