src/Pure/General/pretty.ML
changeset 9841 ca3173f87b5c
parent 9730 11d137b25555
child 10952 b520e4f1313b