src/Pure/General/pretty.ML
changeset 24150 ed724867099a
parent 23922 707639e9497d
child 24612 d1b315bdb8d7