src/Pure/Syntax/syntax_trans.ML
changeset 42889 412fe70f41a4
parent 42476 d0bc1268ef09
child 43326 47cf4bc789aa
equal deleted inserted replaced
42888:4da581400b69 42889:412fe70f41a4