src/HOL/ex/PiSets.thy
changeset 5911 7da8033264fa
parent 5856 5fb5a626f3b9
child 10212 33fe2d701ddd