src/Pure/Syntax/pretty.ML
changeset 4874 c66a42846887
parent 3741 daa5ac720678
child 5230 fdc28193ccf7
equal deleted inserted replaced
4873:b5999638979e 4874:c66a42846887