Email Gateway (Aug 18 2022 at 12:40): Email Gateway (Aug 18 2022 at 12:40):From: Liu Jian <gjk.liu@gmail.com>
Dear all,
How to load HOL4 theories? For example,
theory foo
imports HOL4 Main
.....
reply>> *** could not find theroy file "HOL4.thy" in
/usr/local/Isabelle2008/src/HOL/Library",...
But, HOL4.thy existes in directory "../src/HOL/ImportHOL/"
Cheers,
Liu Jian
Email Gateway (Aug 18 2022 at 12:40):From: Tobias Nipkow <nipkow@in.tum.de>
Liu Jian schrieb:
Sure, but the "could not find in ..." told you Isabelle is not looking
there. If you want to import something from a non-standard location, you
have to give the path explicitly:
imports "..../HOL4"
Unfortunately I just tried but got an I/O error half way through. It may
be that we have allowed those theories to fall into disrepair.
Tobias
Last updated: May 03 2024 at 12:27 UTC