src/Pure/config.ML
changeset 75994 f0ea03be7ceb
parent 74561 8e6c973003c8
child 76058 d45a45eb1aee
equal deleted inserted replaced
75993:8f1bb89ddf4b 75994:f0ea03be7ceb