src/Tools/project_rule.ML
changeset 52265 bb907eba5902
parent 33368 b1cf34f1855c
equal deleted inserted replaced
52264:cdba0c3cb4c2 52265:bb907eba5902