src/HOL/IMP/Collecting.thy
changeset 58255 9dfe8506c04d
parent 55601 b7f4da504b75
child 61179 16775cad1a5c