src/HOL/Imperative_HOL/Imperative_HOL.thy
changeset 80180 e83b1489f4f2
parent 63167 0909deb8059b