> 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 was taught at school to avoid
> On 16 Jan 2018, at 14:13, Blanchette, J.C. 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
> On 11 Jan 2018, at 16:44, Tobias Nipkow wrote:
>
> There are a number of different points here.
>
> - What is good style depends on what your math look like. Knuth writes nice
> traditional math, whereas Isabelle proof states can get quite ugly. In such
> cases I find that
On Di, 2018-01-16 at 16:31 +, Lawrence Paulson wrote:
> I know how to do it, but no beginner could ever find this.
> Larry
This is usually one of the first things I show students learning
Isabelle ... I'm using brackets syntax in demos, but letÂ
them decide which syntax they like better.
Peter
On 16/01/18 16:14, Lawrence Paulson wrote:
On 16 Jan 2018, at 14:13, Blanchette, J.C. 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
I know how to do it, but no beginner could ever find this.
Larry
> On 16 Jan 2018, at 16:20, Andreas Lochbihler
> wrote:
>
> It's not too hard: Go to Plugins/Plugin Options/Isabelle/General and enter
> "brackets" under Print mode.