src/HOL/Library/Imperative_HOL.thy
changeset 29120 8a904ff43f28
parent 27656 d4f6e64ee7cc