src/HOL/ex/PiSets.ML
changeset 5253 82a5ca6290aa
parent 5250 1bff4b1e5ba9
child 5318 72bf8039b53f