On 16/01/18 16:14, Lawrence Paulson wrote:
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 ==>

is actually much more readable than

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

I agree with Larry. I also prefer to write

  ==> bar

because my assumptions are often very long and I want to spot the conclusion 

        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.

It's not too hard: Go to Plugins/Plugin Options/Isabelle/General and enter "brackets" under Print mode.

isabelle-dev mailing list

Reply via email to