Bill, On Jan 6, 2013, at 6:18 AM, Bill Richter <[email protected]> wrote:
> Thanks, Ramana! I'll try to find Larry's book ($66.30 on Amazon). One caution: Larry's (excellent) book is about Standard ML, which is the metalanguage used in HOL IV and ProofPower. HOL Light is implemented in OCaml. With a few notable exception HOL Light generally uses language features that have semantic equivalents in Standard ML, but the syntax is different. If you go to caml.org you will find lots of information and references specific to OCaml. Regards, Rob. ------------------------------------------------------------------------------ Master Visual Studio, SharePoint, SQL, ASP.NET, C# 2012, HTML5, CSS, MVC, Windows 8 Apps, JavaScript and much more. Keep your skills current with LearnDevNow - 3,200 step-by-step video tutorials by Microsoft MVPs and experts. ON SALE this month only -- learn more at: http://p.sf.net/sfu/learnmore_123012 _______________________________________________ hol-info mailing list [email protected] https://lists.sourceforge.net/lists/listinfo/hol-info
