src/Pure/General/pretty.ML
changeset 24058 81aafd465662
parent 23922 707639e9497d
child 24612 d1b315bdb8d7