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

Larry
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Reply via email to