src/HOL/ex/PiSets.ML
changeset 7141 a67dde8820c0
parent 5865 2303f5a3036d
child 9190 b86ff604729f