2016-07-08 09:59:32 UTC
I'm new to isabelle/hol, and I'm currently figuring out how I might use
the system for interactive theorem proving under Linux.
I'm not entirely new to formal proofs, I have a bit of experience
Now my question:
I can't use GUIs for technical reasons, and prefer to do stuff in the
From reading isabelle documentation and grepping through this list's
archives I understand that there is no real user interface for text
terminals (anymore?). Is that correct?
I found isabelle process and isabelle console, but it seems, they are
not intended for manual use. :)
What would be the best approximation to a REPL interface (e.g. like the one
that coqtop provides), for isabelle/hol?
Or maybe I overlooked something and a interactive system can be
easily instanciated from isabelle console?
Thank you very much,