Hi, I thought I would give this a try (I know nothing about Isabelle or HOL). So I downloaded the executable at http://isabelle.in.tum.de/website-Isabelle2016-RC3/ and then ran ./Isabelle2016-RC3
At first it started building loads of files but I ran out of memory so had to stop that building. Then I noticed a src/Tools/SML/Examples.thy in the "Examples" dropdown in the "Documentation" tab on the right. So clicking this opens the file, but I am not sure how to compile and run this file. I looked at some online videos but they didnt really help. So how do I compile and run the src/Tools/SML/Examples.thy file?
Thanks
On Mon, Feb 1, 2016 at 7:07 PM, Makarius <makarius at sketis.net> wrote:
Dear users of the best unknown programming language in the world.
Isabelle/ML is based on Poly/ML and thus benefits from the source-level debugger of that implementation of Standard ML. The Prover IDE provides the Debugger dockable to connect to running ML threads, inspect the stack frame with local ML bindings, and evaluate ML expressions in a particular run-time context.
More explanations with a screenshot on http://sketis.net/2016/ml-debugging-within-the-prover-ide
Makarius
polyml mailing list polyml at inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml