src/Pure/config.ML
changeset 70820 77c8b8e73f88
parent 69576 cfac69e7b962
child 74561 8e6c973003c8
equal deleted inserted replaced
70819:ed89f20de7ab 70820:77c8b8e73f88