src/HOL/ex/PiSets.ML
changeset 8145 cdd5386eb6fe
parent 5865 2303f5a3036d
child 9190 b86ff604729f