src/HOL/HOLCF/IMP/HoareEx.thy
changeset 79905 1f509d01c9e3
parent 76987 4c275405faae
child 80914 d97fdabd9e2b