On 22/02/2019 16:47, Manuel Eberl wrote:
> I came upon a regrssion with the position information in terms that
> contain calligraphic or Fraktur letters, e.g.:
>
> theory Scratch
> Β imports Pure
> begin
>
> lemma "π π π π ()) a b c d e"
>
> The syntax error in this line is at the second closing
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})
I came upon a regrssion with the position information in terms that
contain calligraphic or Fraktur letters, e.g.:
theory Scratch
Β imports Pure
begin
lemma "π π π π ()) a b c d e"
The syntax error in this line is at the second closing parenthesis. In
3bfa28b3a5b2, Isabelle/jEdit displays the er
