Re: [isabelle] Probelm with the "definition" command

Jesus, this is a known problem. If you are OK with inputting the matrix on the
ML level, just stick with it. Alternatively you can look at
where some constants are defined at the ML level (in "Archives/*.ML") but
imported into Isabelle (as Tri, Quad etc). This way you may not need to edit any
generated ML code by hand.


Am 29/04/2013 18:01, schrieb Jesus Aransay:
> Dear all,
> as a different but related issue to my previous mail, when we try to
> input matrices of dimension over 250 * 250 (approx) as elements of
> type "iarray" (the IArray constructor is applied to lists,
> in
> Isabelle (Isabelle/JEdit 2013), by means of the "definition" command,
> processing time gets really slow (of the order of minutes) until the
> editor crashes or we just give it up. Inputting the matrices directly
> in the generated SML code works well.
> Is there any way to improve this behavior?
> Thanks for any hints,
> Jesus
> --
> Jesús María Aransay Azofra
> Universidad de La Rioja
> Dpto. de Matemáticas y Computación
> tlf.: (+34) 941299438 fax: (+34) 941299460
> mail: jesus-maria.aransay at ; web:
> Edificio Luis Vives, c/ Luis de Ulloa s/n, 26004 Logroño, España

This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.