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,
is actually much more readable than
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
I agree with Larry. I also prefer to write
because my assumptions are often very long and I want to spot the conclusion
It's not too hard: Go to Plugins/Plugin Options/Isabelle/General and enter "brackets"
under Print mode.
foo ==> bar
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