src/Pure/General/pretty.ML
changeset 73814 c8b4a4f69068
parent 72075 9c0b835d4cc2
child 74231 b3c65c984210