src/Pure/Syntax/printer.ML
changeset 10618 5b96bc5fbec3
parent 9910 f025cf787554
child 11795 12a0fb3ac366
equal deleted inserted replaced
10617:adc0ed64a120 10618:5b96bc5fbec3