Re: [isabelle] Isabelle2021-1-RC2: Invoking smt-method in theory loaded via Isabelle/Scala

We have another application for grading Isabelle theories on


Am Di., 9. Nov. 2021 um 16:36 Uhr schrieb Makarius <makarius at>:
On 09/11/2021 14:36, Dominique Unruh wrote:
> scala-isabelle actually makes things easier because it encapsulates the
> undocumented (or documented-by-source-code) aspects of the invocation of
> Isabelle into a documented API (that also changes less).

The Isabelle/PIDE server does have a lot of explicit documentation: chapter 4
of the "system" manual. In retrospect, I am unsure if it ever got used in
applications so far.

There is a report by  Boris Shminke on using it from Python: --- but it
remains unclear if and how it works in applications.


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