src/HOL/ex/PiSets.thy
changeset 5393 7299e531d481
parent 5250 1bff4b1e5ba9
child 5846 d99feda2d226