I’d be in favour!
Larry
> On 23 Feb 2019, at 15:07, Makarius wrote:
>
> It might be better to introduce a proof-local version of 'abbreviation'.
___
isabelle-dev mailing list
isabelle-...@in.tum.de
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 wrote:
>>
>> I for one almost always do
>>
>> define G where "G =
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 wrote:
>
> I for one almost always do
>
> define G where "G = homology_group 0 (subtopology (nsphere 0) {pp})"
>
> in
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
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?
Recall this recent thread on
The point is the line breaking. Look at the occurrence of d before the =. This
applies to all infix operators, not just relations.
Larry
> On 22 Feb 2019, at 17:10, Tobias Nipkow wrote:
>
> We had already discussed this and decided that for "=", "<=" etc it makes
> sense.
>
> I find that the
We had already discussed this and decided that for "=", "<=" etc it makes sense.
I find that the wrong associativity can be much more of a killer than where the
infix op is placed.
Tobias
On 22/02/2019 17:20, Lawrence Paulson wrote:
The pretty printing of infix operators looks pretty
