src/Pure/more_pattern.ML
changeset 76243 02c1ffc23d95
parent 74525 c960bfcb91db
child 79242 b0774e7d1949
equal deleted inserted replaced
76242:d704efeb01db 76243:02c1ffc23d95