src/Pure/General/pretty.ML
changeset 52527 dbac84eab3bc
parent 51570 3633828d80fc
child 52693 6651abced106