src/Pure/Syntax/syntax_trans.ML
changeset 42592 fa2cf11d6351
parent 42476 d0bc1268ef09
child 43326 47cf4bc789aa
equal deleted inserted replaced
42591:f139d0ac2d44 42592:fa2cf11d6351