src/Pure/pattern.ML
changeset 59816 034b13f4efae
parent 59026 30b8a5825a9c
child 63718 600cf5c8f2ba
equal deleted inserted replaced
59815:cce82e360c2f 59816:034b13f4efae