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
