src/Pure/Tools/invoke.ML
changeset 21507 f67b41110edd
parent 21483 e4be91feca50
child 21584 22c9392de970