[isabelle-dev] NEWS: op <infix> -> (<infix>)

[Lawrence Paulson]

> On 10 Jan 2018, at 21:26, Makarius <makarius at sketis.net> wrote:
> 
> The Haskell community appears to have picked up a lot of such (slightly
> odd) styles from Lamport. E.g. they put commas at the start of the line
> instead of the end, which is typographically very strange.
> 
> I was educated by the original TeX Book, which in turn refers to the
> top-quality mathematical typesetting from around 1900. Here the
> operators and commas are in the traditional position: end of line.

I got in the habit of putting arithmetic operators at the start of a line while at university, having made too many errors from forgetting that the symbol at the end of the previous line was a minus sign. Of course, that consideration doesn't apply to commas, and it's amazing that Lamport (and Dijkstra?) managed to persuade people to adopt such crazy conventions.

Interactive theorem proving isn't the same thing as solving physics problems by hand, so I'm not against having operators at the end of the line if that's what people think would be best. Note however that the equals sign is an infix operator and is invariably put at the start of a line, never at the end.

Larry