Re: [isabelle] FOL.thy

I am not sure what did you do to trigger this error, but for most purposes you don't need to load FOL.thy yourself. FOL is a part of the ZF set theory logic image, which you can get pre-built from our download page.

Larry Paulson

On 24 Mar 2006, at 09:59, Paqui Lucio wrote:

The file FOL.thy yields the following error in the line 27:
	use "cladata.ML"
The error message is:
*** exception TERM raised: Stale theory encountered:
*** {ProtoPure, Pure, #, !}
*** At command "use".

Please, could someone tell me what can I do?

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