Re: [isabelle] load HOL4
Liu Jian schrieb:
> Dear all,
> How to load HOL4 theories? For example,
> theory foo
> imports HOL4 Main
> reply>> *** could not find theroy file "HOL4.thy" in
> But, HOL4.thy existes in directory "../src/HOL/ImportHOL/"
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:
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and