Marko, Petros & Ramana, I use Emacs & miz3, with a minimal interface hol_light/RichterHilbertAxiomGeometry/hol-light-fonts.el which mostly allows writing HOL Light code with math characters. The Isabelle folks are phasing out ProofGeneral in favor of jedit. I would like to have automatic indentation, so TAB would move you where in the correctly indented place. I've seen this for Scheme code. I imagine that's only a few lines of Emacs code, but I haven't written it. Another Emacs point is that evaluating code in an Emacs shell is a good idea, because you can then look at thousands of lines of output: there's no scroll limit. Freek's paper arxiv.org/pdf/1201.3601 sorta gives the impression that you need an interface to use miz3, but you can just paste code from your editor into the window running ocaml. I don't know what the HOL4 Emacs support does.
-- Best, Bill ------------------------------------------------------------------------------ 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
