src/Pure/General/pretty.ML
changeset 59122 c1dbcde94cd2
parent 56334 6b3739fee456
child 61862 e2a9e46ac0fb
equal deleted inserted replaced
59121:8ea2748241da 59122:c1dbcde94cd2