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