Better tutorial/examples needed

[geneing]

trafficstars

Are there any more extensive tutorial available? I only see "hello world" example, and it only seems to show how to run a single thy file.

Looking at the code there must be more functionality provided by the library. What does this library do? Can one use this library to submit proof statement by statement to isabelle and get back diagnostics?

Are there projects that use libisabelle that I could use as example?

[larsrh]

What does this library do?

In a nutshell:

• install Isabelle uniformly on the supported platforms
• act as a package manager for Isabelle formalizations (in conjunction with sbt-libisabelle
• provide an RPC layer between Scala/Java/JVM code and Isabelle/ML

The most extensive tool that uses this library is Leon. To get an overview over what this tool does (and how it uses libisabelle), check out the paper.

Can one use this library to submit proof statement by statement to isabelle and get back diagnostics?

That greatly depends on what you mean by "diagnostics". Do you want to prove statements? Find counterexamples?