Ramana wrote: | HOL-Omega has type quantification, and is backwards compatible with | HOL4. http://www.trustworthytools.com/id17.html.
Norbert Voelker's HOL2P also offers type quantification, and is essentially upward compatible with HOL Light: http://cswww.essex.ac.uk/staff/norbert/hol2p/ Indeed, as Peter Homeier has noted, HOL2P was a major inspiration for his own further extension of the type theory in HOL-Omega. 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
