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.

Tobias





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