src/Pure/display.ML
changeset 21404 eb85850d3eb7
parent 20629 8f6cc81ba4a3
child 21646 c07b5b0e8492