src/HOL/IMP/Collecting_Examples.thy
changeset 58476 6ade4c7109a8
parent 52019 a4cbca8f7342
child 67406 23307fd33906