src/Pure/General/pretty.ML
changeset 70299 83774d669b51
parent 69345 6bd63c94cf62
child 71465 910a081cca74