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