src/Pure/General/pretty.ML
changeset 32405 48786f277130
parent 30667 53fbf7c679b0
child 32738 15bb09ca0378