src/Pure/POLY.ML
changeset 1868 836950047d85
parent 1480 85ecd3439e01
child 2141 c2aedd8169cd