[isabelle-dev] Spec_Check

Makarius makarius at sketis.net
Thu May 30 23:27:04 CEST 2013

There is a funny comment here:

   (* Isabelle does not use vectors? *)

Isn't live nice without vectors, arrays, a host of "int" types that are 
not int at all?

The one exception is src/Pure/Syntax/parser.ML, where arrays are used 
internally due to some historic "optimization".  It probably wastes a lot 
of space, since every grammar update needs a fresh copy of the whole 

Working routinely on the JVM now (due to Scala), I've found so many 
inefficiencies in the libraries due to the historic predominance of these 
mutable bulk data structures (aka arrays).  This is particularly bad when 
working with plain text, aka strings.


More information about the isabelle-dev mailing list