[isabelle-dev] BNF: number of dead variables

[Makarius]

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
----------------------------------------------------------------------------