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