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

[Lawrence Paulson]

> On 16 Jan 2018, at 14:13, Blanchette, J.C. <j.c.blanchette at vu.nl> wrote:
> 
> However, for operators like ==>, which bind on the right,
> 
> 	foo ==>
> 	bar
> 
> is actually much more readable than
> 
> 	foo
> 	==> bar

This sort of claim needs to be justified by evidence. We had it the first way until the late 1990s. I changed it to the other way while working on large proof states connected with crypto protocols. It seemed more readable to me for such proofs.

> 	foo ==> bar
> 	==> baz

As for this last example, we definitely need the earlier syntax [|foo; bar|] ==> baz, which has been made almost impossible to enable.

Larry