src/Pure/Syntax/pretty.ML
changeset 430 89e1986125fe
parent 261 3441647c8c90
child 512 55755ed9fab9