src/HOL/Library/Imperative_HOL.thy
changeset 28562 4e74209f113e
parent 27656 d4f6e64ee7cc