src/HOL/Library/Imperative_HOL.thy
changeset 27885 76b51cd0a37c
parent 27656 d4f6e64ee7cc