src/HOL/ex/PiSets.ML
changeset 5479 5a5dfb0f0d7d
parent 5318 72bf8039b53f
child 5521 7970832271cc