src/HOL/Imperative_HOL/Imperative_HOL.thy
changeset 37724 6607ccf77946
parent 29822 c45845743f04
child 37772 026ed2fc15d4