Re: [isabelle-dev] NEWS: op -> ()

2018-01-16 Thread Blanchette, J.C.
> 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

Re: [isabelle-dev] NEWS: op -> ()

2018-01-16 Thread Lawrence Paulson
> 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

Re: [isabelle-dev] NEWS: op -> ()

2018-01-16 Thread Blanchette, J.C.
> 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

Re: [isabelle-dev] NEWS: op -> ()

2018-01-16 Thread Peter Lammich
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

Re: [isabelle-dev] NEWS: op -> ()

2018-01-16 Thread Andreas Lochbihler
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

Re: [isabelle-dev] NEWS: op -> ()

2018-01-16 Thread Lawrence Paulson
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.