src/HOL/Imperative_HOL/Array.thy
changeset 46264 f575281fb551
parent 40671 5e46057ba8e0
child 48073 1b609a7837ef