[isabelle-dev] NEWS: op <infix> -> (<infix>)

Andreas Lochbihler andreas.lochbihler at inf.ethz.ch
Tue Jan 16 17:20:31 CET 2018

On 16/01/18 16:14, Lawrence Paulson wrote:
>> On 16 Jan 2018, at 14:13, Blanchette, J.C. <j.c.blanchette at 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

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


More information about the isabelle-dev mailing list