For whom efficient code is a concern: * Library/IArray.thy: immutable arrays with code generation. Tobias