src/Pure/General/pretty.ML
changeset 27940 002718f9c938
parent 27351 6b120fb45278
child 29606 fedb8be05f24