src/HOL/IMP/Collecting1.thy
changeset 47108 2a1953f0d20d
parent 46334 3858dc8eabd8
child 52019 a4cbca8f7342