src/Pure/Syntax/simple_syntax.ML
changeset 27885 76b51cd0a37c
parent 27802 1eddcd7dda2d
child 27888 7ed38f1d11de