src/HOL/IMP/Denotation.thy
changeset 3581 0727ebd62b48
parent 2847 6226b83ce2d8
child 4897 be11be0b6ea1