src/Pure/Syntax/syntax.ML
changeset 43599 e0ee016fc4fd
parent 43558 94a08fb3ae4a
child 43731 70072780e095