src/Pure/General/pretty.ML
changeset 18768 6e97b57cdcba
parent 18603 04c2c702a3fb
child 18802 f449d516f36b