src/Pure/Syntax/syntax.ML
changeset 2348 b51e104ecf40
parent 2287 94b70aeb7d1f
child 2366 a163d2be1bb5