Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] FOL.thy

view this post on Zulip Email Gateway (Aug 17 2022 at 14:15):

From: Paqui Lucio <paqui.lucio@ehu.es>
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?
Paqui

Last updated: May 03 2024 at 04:19 UTC