src/Pure/Syntax/syntax_trans.ML
changeset 43956 4611af362cd0
parent 43326 47cf4bc789aa
child 44241 7943b69f0188
equal deleted inserted replaced
43955:efc6f0a81c36 43956:4611af362cd0