[isabelle-dev] BNF: number of dead variables

[Jasmin Christian Blanchette]

Am 15.12.2014 um 17:48 schrieb Makarius <makarius at sketis.net>:

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

I actually find this name somewhat ambiguous. Isabelle/ML sounds to me like a "slice" of Isabelle when viewed through an ML programmer's goggles. This is, I believe, how the term has been used until 2014. Something like SML/Isabelle or SML_{Isabelle} would sound more like a programming language (although I'm not seriously advocating any of these right now).

For the title of that particular section, the "Standard ML" part is supposed to add one bit of information. I could dodge the issue by writing "Programmatic" (and do the same in the Nitpick manual).

Jasmin