src/Pure/General/pretty.ML
changeset 46393 69f2d19f7d33
parent 45666 d83797ef0d2d
child 46894 e2ad717ec889