src/Pure/pattern.ML
changeset 14319 255190be18c0
parent 13998 75a399c2781f
child 14643 130076a81b84
equal deleted inserted replaced
14318:7dbd3988b15b 14319:255190be18c0