src/Tools/project_rule.ML
changeset 31801 b97b34e7c853
parent 31794 71af1fd6a5e4
child 32172 c4e55f30d527
equal deleted inserted replaced
31800:477f2abf90a4 31801:b97b34e7c853