src/Pure/General/path.ML
changeset 18703 13e11abcfc96
parent 17827 b32fad049413
child 19305 5c16895d548b
equal deleted inserted replaced
18702:7dc7dcd63224 18703:13e11abcfc96