src/Pure/Syntax/syn_trans.ML
changeset 4962 e9217cb15b42
parent 4700 20ade76722d6
child 5084 a676ada3b380
equal deleted inserted replaced
4961:27f559b54c57 4962:e9217cb15b42