[isabelle] Probelm with the "definition" command

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,
http://isabelle.in.tum.de/library/HOL/HOL-Library/IArray.html) 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,


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 unirioja.es ; web: http://www.unirioja.es/cu/jearansa
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.