src/Pure/config.ML
changeset 59010 ec2b4270a502
parent 58951 8b7caf447357
child 63806 c54a53ef1873
equal deleted inserted replaced
59009:348561aa3869 59010:ec2b4270a502