src/Pure/General/pretty.ML
changeset 58161 deeff89d5b9e
parent 56334 6b3739fee456
child 61862 e2a9e46ac0fb