src/Pure/library.ML
changeset 5601 b6456ccd9e3e
parent 5285 2d1425492fb3
child 5893 c755dfd02509
equal deleted inserted replaced
5600:34b3366b83ac 5601:b6456ccd9e3e