src/Pure/Tools/print_operation.ML
changeset 62842 db9f95ca2a8f
parent 61223 dfccf6c06201
child 64677 8dc24130e8fe