src/HOL/Imperative_HOL/Array.thy
changeset 73255 7e2a9a8c2b85
parent 73137 ca450d902198
child 77106 5ef443fa4a5d