src/Pure/Syntax/syntax.ML
changeset 43655 5742b288bb86
parent 43558 94a08fb3ae4a
child 43731 70072780e095