src/Pure/Syntax/syntax_trans.ML
changeset 45771 a70465244096
parent 45389 bc0d50f8ae19
child 46236 ae79f2978a67
equal deleted inserted replaced
45770:5d35cb2c0f02 45771:a70465244096