src/Pure/General/pretty.ML
changeset 51685 385ef6706252
parent 51570 3633828d80fc
child 52693 6651abced106