src/HOL/IMP/Collecting.thy
changeset 56262 251f60be62a7
parent 55601 b7f4da504b75
child 61179 16775cad1a5c