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 <makar...@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@inf.ed.ac.uk > http://lists.inf.ed.ac.uk/mailman/listinfo/polyml >
_______________________________________________ polyml mailing list polyml@inf.ed.ac.uk http://lists.inf.ed.ac.uk/mailman/listinfo/polyml
