src/Pure/Syntax/pretty.ML
changeset 2348 b51e104ecf40
parent 2149 639db8177804
child 2695 871b69a4b78f