src/HOL/IMP/Denotation.thy
changeset 17601 a6a322f96145
parent 16417 9bc16273c2d4
child 18372 2bffdf62fe7f