src/Pure/Syntax/syntax.ML
changeset 36696 1b69f78be286
parent 36610 bafd82950e24
child 36739 e9401d2efc5f