src/HOL/IMP/Hoare_Total_EX.thy
changeset 71751 abf3e80bd815
parent 69505 cc2d676d5395
child 74500 40f03761f77f