src/Pure/config.ML
changeset 70904 caf91f9b847b
parent 69576 cfac69e7b962
child 74561 8e6c973003c8
equal deleted inserted replaced
70899:5f6dea6a7a4c 70904:caf91f9b847b