[isabelle-dev] infix line breaking

[Makarius]

On 23/02/2019 12:25, Lawrence Paulson wrote:
> Which reminds me: I define such abbreviations all the time, using “let”. Could let-abbreviations be folded upon printing?
> 
>> 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})"

It might be better to introduce a proof-local version of 'abbreviation'.


	Makarius