[isabelle-dev] infix line breaking

[Lawrence Paulson]

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