src/Pure/Syntax/syn_ext.ML
changeset 33145 1a22f7ca1dfc
parent 32785 ec5292653aff
child 33037 b22e44496dc2
equal deleted inserted replaced
33144:1831516747d4 33145:1a22f7ca1dfc