[isabelle] Isabelle and the text console


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
with coq.

Now my question:
I can't use GUIs for technical reasons, and prefer to do stuff in the
shell anyways.

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,


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