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