src/HOL/ex/PiSets.thy
changeset 9380 63cca60b2cce
parent 5856 5fb5a626f3b9
child 10212 33fe2d701ddd