src/Pure/Syntax/syntax.ML
changeset 24547 64c20ee76bc1
parent 24512 fc4959967b30
child 24613 bc889c3d55a3