src/Pure/Syntax/pretty.ML
changeset 4962 e9217cb15b42
parent 3741 daa5ac720678
child 5230 fdc28193ccf7