src/Pure/General/pretty.ML
changeset 51685 385ef6706252
parent 51570 3633828d80fc
child 52693 6651abced106
equal deleted inserted replaced
51671:0d142a78fb7c 51685:385ef6706252