src/Pure/General/pretty.ML
changeset 33178 70522979c7be
parent 32966 5b21661fe618
child 36687 58020b59baf7