[isabelle-dev] [isabelle] TYPE_MATCH exception with adhoc_overloading

[Makarius]

On Mon, 19 Jan 2015, Jasmin Blanchette wrote:

>> Just a reminder that this old thread is not yet resolved and currently 
>> I'm essentially stuck.
>
> I hope somebody who has a clue will answer your email.

I still have various "important" markers on this mail thread, to see if I 
can tell something about it, but I did not manage to pick it up again. 
It will happen really soon now ...


>> drop_semicolons
>
> I’ve applied and push your first change.
>
> As for semicolon, the standard style is rather to put them, not to drop 
> them.

Strictly speaking there is no standard for semicolons in Isabelle/ML, only 
the universal standard of uniformity: a file either has extra semicolons 
or does not have extra semicolons.


More than 20 years ago, semicolons where generally en-vogue, and no 
surprise for me in SML.  Then they became less popular, e.g. in Scala we 
now see sophisticated rules for implicit "semicolon inference".  The Isar 
language has lost its semicolon altogether some weeks ago (5ff61774df11).

Over the decades I have occasionally experimented with writing less 
semicolons in ML, but each time I ran into practical inconveniences 
concerning error situations (broken partial input), and closed ML modules 
versus open sequences of declarations (e.g. in the 'ML' command).

My present style of doing it (approx. the last 10 years) is somehow 
optimized in that respect.  Whenever I do serious renovations on some old 
ML module, I first normalize the semicolon style (and other styles as 
well), just to save a lot of time in the actual work.


 	Makarius