src/Pure/General/pretty.ML
changeset 23024 70435ffe077d
parent 22019 0b7aff48622e
child 23617 840904fc1eb1