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-...@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
