src/Pure/General/pretty.ML
changeset 74177 a8b032dede5c
parent 72075 9c0b835d4cc2
child 74231 b3c65c984210