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

[Jasmin Blanchette]

Hi Chris,

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

> Independent of my being stuck, could one of the devs apply at least the first of the following attached patches (and the second one depending on whether dropping semicolons is in general seen as good style or not) that somehow drowned in previous emails:
> 
> delete
> 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. I personally prefer not to have them, because it’s easier to standardize on dropping them than on adding them everywhere, but as they say, there is no I in "team". ;)

My rule of thumb would be: Try to be locally consistent. For example, Nitpick, Sledgehammer and SMT don’t use semicolons (and adding them now would be a pain); but BNF does use them.

Cheers,

Jasmin