src/HOL/Library/SetsAndFunctions.thy
changeset 17076 c7effdf2e2e2
parent 16932 0bca871f5a21
child 17161 57c69627d71a