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



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:
https://link.springer.com/chapter/10.1007%2F978-3-030-81097-9_20 --- but it
remains unclear if and how it works in applications.


	Makarius




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