There are at least some efforts afoot to support HOL Light in Proof General:

  http://proofgeneral.inf.ed.ac.uk/releases/ProofGeneral-latest/hol-light/

>From the README file:

  This is a "technology demonstration" of Proof General for HOL-Light.

  We have written this in the hope that somebody from the HOL-Light
  community will adopt it, maintain and improve it, and thus turn it
  into a proper instantiation of Proof General.

John.

------------------------------------------------------------------------------
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/learnnow-d2d
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info

Reply via email to