src/Pure/General/pretty.ML
changeset 50357 187ae76a1757
parent 50201 c26369c9eda6
child 50545 00bdc48c5f71
equal deleted inserted replaced
50356:41f8f1f2e15d 50357:187ae76a1757