src/Pure/General/pretty.ML
changeset 6845 598d2f32d452
parent 6321 207f518167e8
child 8456 8ccda76f07cb
equal deleted inserted replaced
6844:3909657a7da6 6845:598d2f32d452