src/HOL/IMP/Collecting_Examples.thy
changeset 59162 dca5594761f2
parent 52019 a4cbca8f7342
child 67406 23307fd33906