src/HOL/Library/Imperative_HOL.thy
changeset 29412 4085a531153d
parent 27656 d4f6e64ee7cc