src/Pure/General/pretty.ML
changeset 17184 3d80209e9a53
parent 16714 d9e3ef66b38c
child 17400 6ede71a506f5
equal deleted inserted replaced
17183:a788a05fb81b 17184:3d80209e9a53