[isabelle-dev] infix line breaking

[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 in HOL-Algebra become
totally unreadable in my experience.

Manuel


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-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev