src/Pure/config.ML
changeset 41683 73dde8006820
parent 40291 012ed4426fda
child 47814 53668571d300
equal deleted inserted replaced
41682:44a2e0db281f 41683:73dde8006820