src/HOL/IMP/Collecting_Examples.thy
changeset 66787 64b47495676d
parent 52019 a4cbca8f7342
child 67406 23307fd33906