src/Tools/project_rule.ML
changeset 54957 99eebac5fcb3
parent 33368 b1cf34f1855c
equal deleted inserted replaced
54956:80a1931267ce 54957:99eebac5fcb3