src/Pure/General/pretty.ML
changeset 31060 75d7c7cc8bdb
parent 30667 53fbf7c679b0
child 32738 15bb09ca0378
equal deleted inserted replaced
31059:45c085c7efc6 31060:75d7c7cc8bdb