src/Pure/General/pretty.ML
changeset 43560 d1650e3720fd
parent 42383 0ae4ad40d7b5
child 43684 85388f5570c4