src/Pure/General/pretty.ML
changeset 68204 a554da2811f2
parent 67522 9e712280cc37
child 68918 3a0db30e5d87