src/Pure/Syntax/syntax.ML
changeset 28500 4b79e5d3d0aa
parent 28413 ee73353fb87c
child 28840 049f0a8faa35