src/Pure/Syntax/syntax.ML
changeset 81656 7593c0976dc6
parent 81601 26ff119fb140
child 81993 f62e7c3ab254