src/HOL/IMP/Collecting.thy
changeset 58935 dcad9bad43e7
parent 55601 b7f4da504b75
child 61179 16775cad1a5c