src/Pure/General/pretty.ML
changeset 69843 edda2d14c108
parent 69345 6bd63c94cf62
child 71465 910a081cca74