src/Pure/General/pretty.ML
changeset 81409 07c802837a8c
parent 81270 b98595f82a88
child 81683 b31d09029b94