I'm using HOL4 in the Windows console. I load a file using the "use" command, like this:
use "E:/E_main2/binp/HOL4k7/examples/euclid.sml"; I then edit some ML scripts in an editor and load them into HOL4 using the "use" command. My scripts get errors, so when I try to load "euclid.sml" again as shown above, I get errors in HOL4 which I didn't get before. I close the HOL4 window, and then start HOL4 again, but it doesn't start up instantly. Is there a command I can use to reinitialize HOL4 without closing it and restarting it? Thanks, GB ------------------------------------------------------------------------------ Live Security Virtual Conference Exclusive live event will cover all the ways today's security and threat landscape has changed and how IT managers can respond. Discussions will include endpoint security, mobile security and the latest in malware threats. http://www.accelacomm.com/jaw/sfrnl04242012/114/50122263/ _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
