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
https://mailmanbroy.informatik.tu-muenchen.de/mailman
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 = homology_grou
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 suc
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 tha
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 terribl
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})