> On 16 Jan 2018, at 14:13, Blanchette, J.C. <j.c.blanche...@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.

isabelle-dev mailing list

Reply via email to