src/HOL/Imperative_HOL/Array.thy
changeset 42230 594480d25aaa
parent 40671 5e46057ba8e0
child 48073 1b609a7837ef