src/Tools/project_rule.ML
changeset 57830 2d0f0d6fdf3e
parent 33368 b1cf34f1855c
equal deleted inserted replaced
57829:b1113689622b 57830:2d0f0d6fdf3e