src/HOL/IMP/Hoare_Total_EX.thy
changeset 67946 e1e57c288e45
parent 67406 23307fd33906
child 68776 403dd13cf6e9