src/HOL/Set.thy
changeset 9789 7e5e6c47c0b5
parent 8148 5ef0b624aadb
child 10106 1b63e30437ee