src/HOL/IMP/Collecting.thy
changeset 50363 2f8dc9e65401
parent 49604 c54d901d2946
child 51039 3775bf0ea5b8