src/Pure/General/pretty.ML
changeset 53226 9cf8e2263ca7
parent 52693 6651abced106
child 55033 8e8243975860
equal deleted inserted replaced
53214:bae01293f4dd 53226:9cf8e2263ca7