src/Pure/Tools/print_operation.ML
changeset 60667 d86c449d30ba
parent 60610 f52b4b0c10c4
child 61212 cb9d0c99bd36