Re: [isabelle-dev] infix line breaking

2019-02-23 Thread Lawrence Paulson
I’d be in favour! Larry > On 23 Feb 2019, at 15:07, Makarius wrote: > > It might be better to introduce a proof-local version of 'abbreviation'. ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman

Re: [isabelle-dev] infix line breaking

2019-02-23 Thread Makarius
On 23/02/2019 12:25, Lawrence Paulson wrote: > Which reminds me: I define such abbreviations all the time, using “let”. > Could let-abbreviations be folded upon printing? > >> On 23 Feb 2019, at 09:10, Manuel Eberl wrote: >> >> I for one almost always do >> >> define G where "G = homology_grou

Re: [isabelle-dev] infix line breaking

2019-02-23 Thread Lawrence Paulson
Which reminds me: I define such abbreviations all the time, using “let”. Could let-abbreviations be folded upon printing? Larry > On 23 Feb 2019, at 09:10, Manuel Eberl wrote: > > I for one almost always do > > define G where "G = homology_group 0 (subtopology (nsphere 0) {pp})" > > in suc

Re: [isabelle-dev] infix line breaking

2019-02-23 Thread Manuel Eberl
I for one almost always do   define G where "G = homology_group 0 (subtopology (nsphere 0) {pp})" in such cases, perhaps occasionally combined with a   note [simp] = G_def [symmetric] at least during the "exploratory" stage of Isar proof writing. Without that, statements and proof obligations

Re: [isabelle-dev] infix line breaking

2019-02-22 Thread Makarius
On 22/02/2019 17:20, Lawrence Paulson wrote: > The pretty printing of infix operators looks pretty terrible in the presence > of large terms. > > I’d like to propose having infix operators breaking at the start of the line > rather than at the end. Any thoughts? Recall this recent thread on tha

Re: [isabelle-dev] infix line breaking

2019-02-22 Thread Lawrence Paulson
The point is the line breaking. Look at the occurrence of d before the =. This applies to all infix operators, not just relations. Larry > On 22 Feb 2019, at 17:10, Tobias Nipkow wrote: > > We had already discussed this and decided that for "=", "<=" etc it makes > sense. > > I find that the

Re: [isabelle-dev] infix line breaking

2019-02-22 Thread Tobias Nipkow
We had already discussed this and decided that for "=", "<=" etc it makes sense. I find that the wrong associativity can be much more of a killer than where the infix op is placed. Tobias On 22/02/2019 17:20, Lawrence Paulson wrote: The pretty printing of infix operators looks pretty terribl

[isabelle-dev] infix line breaking

2019-02-22 Thread Lawrence Paulson
The pretty printing of infix operators looks pretty terrible in the presence of large terms. I’d like to propose having infix operators breaking at the start of the line rather than at the end. Any thoughts? Larry inv⇘homology_group 0 (nsphere 0)⇙ hom_induced 0 (subtopology (nsphere 0) {pp})