src/HOL/Imperative_HOL/Array.thy
changeset 46556 2848e36e0348
parent 40671 5e46057ba8e0
child 48073 1b609a7837ef