src/HOLCF/IMP/Denotational.thy
changeset 12791 ccc0f45ad2c4
parent 12600 30ec65eaaf5f
child 16417 9bc16273c2d4