src/HOL/IMP/Collecting_Examples.thy
changeset 58711 3f7886cd75b9
parent 52019 a4cbca8f7342
child 67406 23307fd33906