src/HOL/IMP/Hoare_Examples.thy
changeset 59370 b13ff987c559
parent 58410 6d46ad54a2ab
child 61028 99d58362eeeb