<!DOCTYPE html><html><head>
<style type="text/css">body { font-family:'DejaVu Sans Mono'; font-size:12px}</style>
<style type="text/css">body { font-family:'DejaVu Sans Mono'; font-size:12px}</style>
</head>
<body><br><br>------- Forwarded message -------<br>From: Yannick <yannick_duchene@yahoo.fr><br>To: "Ramana Kumar" <ramana@member.fsf.org><br>Cc:<br>Subject: Re: [opentheory-users] Is OpenTheory usable with Coq?<br>Date: Wed, 30 Dec 2015 02:46:31 +0100<br><br>On Tue, 29 Dec 2015 13:25:44 +0100, Ramana Kumar <ramana@member.fsf.org> wrote:<br><br><blockquote style="margin: 0 0 0.80ex; border-left: #0000FF 2px solid; padding-left: 1ex"><div dir="ltr">I should add that for HOL4 (and HOL Light, I think) there are editor-based interfaces (for Vim and for Emacs, at least) so you are not confined to using only the read-eval-print loop.<br></div></blockquote><div><br></div><div>Precisely the two editors I'm afraid of :-D . Don't mind, I will setup what I need if I'm really not OK with the SML interpreter interface.</div><div><br></div><br><div id="M2Signature"><div>-- </div><div>Yannick Duchêne</div></div><br><br><br><div id="M2Signature"><div>-- </div><div>Yannick Duchêne</div></div></body></html>