src/HOL/Imperative_HOL/Array.thy
changeset 30960 fec1a04b7220
parent 29822 c45845743f04
child 31203 5c8fb4fd67e0