src/HOL/IMP/VCG.thy
changeset 55736 f1ed1e9cd080
parent 55003 c65fd9218ea1
child 58249 180f1b3508ed