src/HOL/Imperative_HOL/Imperative_HOL.thy
changeset 32497 922718ac81e4
parent 29822 c45845743f04
child 37772 026ed2fc15d4