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
> /usr/local/Isabelle2008/src/HOL/Library",...
> 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:

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.


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