src/HOL/IMP/Collecting.thy
changeset 56547 e9bb73d7b6cf
parent 55601 b7f4da504b75
child 61179 16775cad1a5c