Re: [isabelle] Another newbie question...case-based proofs
> On 5. Apr 2019, at 12:21, Makarius <makarius at sketis.net> wrote:
> On 12/03/2019 17:15, Wolfgang Jeltsch wrote:
>> By the way, have there been any attempts so far to integrate Isabelle
>> into Vim?
> No, Isabelle is moving in the opposite direction.
As long as Isabelle supports the language server protocol, it is possible to make vim interact with Isabelle (with some limitations; e.g., there are no colours in the equivalent of the 'buffer+output buffer'). However, the integration requires some work. I don't know anything about the internals of vim, but, at least in emacs, the lack of multithreading is an issue.
Otherwise, VSCode probably has a mode with vim keybindings.
> I recommend HOL4 in that respect.
This archive was generated by a fusion of
Pipermail (Mailman edition) and