src/Pure/Syntax/simple_syntax.ML
changeset 27853 916038f77be6
parent 27802 1eddcd7dda2d
child 27888 7ed38f1d11de