src/HOL/Imperative_HOL/Array.thy
changeset 31413 729d90a531e4
parent 31205 98370b26c2ce
child 31870 5274d3d0a6f2