HOL-ex.IArray_Examples