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 ==>
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.
I agree with Larry. I also prefer to write
foo
==> bar
because my assumptions are often very long and I want to spot the conclusion
immediately.
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.
Andreas
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev