Which reminds me: I define such abbreviations all the time, using “let”. Could
let-abbreviations be folded upon printing?
Larry
> On 23 Feb 2019, at 09:10, Manuel Eberl <ebe...@in.tum.de> wrote:
>
> 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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
