src/HOL/IMP/Collecting1.thy
changeset 63297 ce995deef4b0
parent 52019 a4cbca8f7342
child 67406 23307fd33906