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
smime.p7s
Description: S/MIME Cryptographic Signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
