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.


Mathias




> 
> I recommend HOL4 in that respect.
> 
> 
> 	Makarius
> 





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.