src/HOL/IMP/Collecting.thy
changeset 58710 7216a10d69ba
parent 55601 b7f4da504b75
child 61179 16775cad1a5c