src/Pure/General/pretty.ML
changeset 72840 6b96464066a0
parent 72075 9c0b835d4cc2
child 74231 b3c65c984210
equal deleted inserted replaced
72839:a597300290de 72840:6b96464066a0