src/Pure/Syntax/syntax.ML
changeset 6280 218733fb6987
parent 6167 2f354020efc3
child 6322 7047300264c9