src/Pure/Syntax/syntax.ML
changeset 43655 5742b288bb86
parent 43558 94a08fb3ae4a
child 43731 70072780e095
equal deleted inserted replaced
43654:3f1a44c2d645 43655:5742b288bb86