src/Pure/General/path.ML
changeset 46730 e3b99d0231bc
parent 45666 d83797ef0d2d
child 47661 012a887997f3
equal deleted inserted replaced
46729:046ea3c1000e 46730:e3b99d0231bc