On Wed, 3 Dec 2014, Jasmin Christian Blanchette wrote:
Those interfaces were never very polished, nor documented (although I
might come to add a section to "isabelle doc datatypes" about the ML
functions -- there is an embryonic, commented out "Using the Standard ML
Interface" section already).
Just a side-remark: the programming language is called "Isabelle/ML" -- it
is based on Standard ML, but something slightly different.
The distinction of "Isabelle/ML" vs. regular "Standard ML" has become very
relevant in Isabelle2014, since there is now IDE support for the latter,
and people tend to get confused by that as can be seen here:
http://lists.inf.ed.ac.uk/pipermail/polyml/2014-December/001497.html
Makarius
----------------------------------------------------------------------------
http://stop-ttip.org 1,151,632 people so far
----------------------------------------------------------------------------
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
