Hi everyone; I have a huge definition of an RTL design function (more that 6000 lines of HOL code), and I'm trying to load and compile it in HOL, but I couldn't succeed. I first tried to copy and paste from emacs but it didn't work. Then, I made a script file out of the definition together with the related theories but Holmake didn't generate the theory file at the end after taking lots of time. I even tried Magnus and Michael's script for interaction with HOL via emacs/xemacs using C-space and M-h M-r keys, but it didn't work either. Do you have any idea how to solve this problem?
Thanks, Behzad ------------------------------------------------------------------------------ Come build with us! The BlackBerry® Developer Conference in SF, CA is the only developer event you need to attend this year. Jumpstart your developing skills, take BlackBerry mobile applications to market and stay ahead of the curve. Join us from November 9-12, 2009. Register now! http://p.sf.net/sfu/devconf _______________________________________________ hol-info mailing list hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info
