src/HOL/Imperative_HOL/Imperative_HOL.thy
changeset 32705 04ce6bb14d85
parent 29822 c45845743f04
child 37772 026ed2fc15d4