src/Pure/General/source.ML
changeset 27178 c8ddb3000743
parent 25846 f5fb187ae10d
child 27732 8dbf5761a24a
equal deleted inserted replaced
27177:adefd3454174 27178:c8ddb3000743