src/Pure/General/pretty.ML
changeset 14898 a25550451b51
parent 14832 6589a58f57cb
child 14972 51f95648abad