src/Pure/General/pretty.ML
changeset 57978 8f4a332500e4
parent 56334 6b3739fee456
child 61862 e2a9e46ac0fb
equal deleted inserted replaced
57977:113b43b84412 57978:8f4a332500e4