src/Pure/General/pretty.ML
changeset 8970 3ac901561f33
parent 8806 a202293db3f6
child 9121 25245986e667