[isabelle] load HOL4



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 to: gjk.liu at gmail.com





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