src/Pure/Syntax/syntax.ML
changeset 55893 aed17a173d16
parent 55829 b7bdea5336dd
child 56334 6b3739fee456