src/Pure/Tools/print_operation.ML
changeset 57256 cf43583f9bb9
parent 56893 62d237cdc341
child 57415 e721124f1b1e