src/Pure/General/pretty.ML
changeset 9502 50ec59aff389
parent 9121 25245986e667
child 9730 11d137b25555