src/Pure/Syntax/syntax.ML
changeset 25111 d52a58b51f1f
parent 25060 17c313217998
child 25122 f37d7dd25c88
equal deleted inserted replaced
25110:7253d331e9fc 25111:d52a58b51f1f