[isabelle-dev] BNF: number of dead variables

Makarius makarius at sketis.net
Mon Dec 15 17:48:11 CET 2014

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://stop-ttip.org  1,151,632 people so far

More information about the isabelle-dev mailing list