src/Pure/Tools/print_operation.ML
changeset 63789 af28929ff219
parent 61223 dfccf6c06201
child 64677 8dc24130e8fe
equal deleted inserted replaced
63788:3160826b92f8 63789:af28929ff219