src/HOL/IMP/Hoare_Examples.thy
changeset 58255 9dfe8506c04d
parent 54489 03ff4d1e6784
child 58410 6d46ad54a2ab