Am 15.12.2014 um 17:48 schrieb Makarius <makar...@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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
