src/Pure/General/pretty.ML
changeset 38099 e3bb96b83807
parent 37529 a23e8aa853eb
child 38474 e498dc2eb576
equal deleted inserted replaced
38098:db90d313cf53 38099:e3bb96b83807