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 <nip...@in.tum.de> wrote:
>
> 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 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}) {} (nsphere 0) {} r
>> d =
>> hom_induced 0 (subtopology (nsphere 0) {nn}) {} (nsphere 0) {} id
>> (hom_induced 0 (subtopology (nsphere 0) {pp}) {} (subtopology (nsphere
>> 0) {nn}) {} r
>> (inv⇘homology_group 0 (subtopology (nsphere 0) {pp})⇙ d))
>> _______________________________________________
>> isabelle-dev mailing list
>> isabelle-...@in.tum.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-...@in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
