src/Pure/General/pretty.ML
changeset 82302 19ada02fa486
parent 81718 289ded3c342f
child 82316 83584916b6d7