src/Pure/General/pretty.ML
changeset 9619 6125cc9efc18
parent 9121 25245986e667
child 9730 11d137b25555