[isabelle-dev] infix line breaking

Makarius makarius at sketis.net
Sat Feb 23 16:07:12 CET 2019

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


More information about the isabelle-dev mailing list