src/Pure/pattern.ML
changeset 16809 8ca51a846576
parent 16668 fdb4992cf1d2
child 16939 87fc64d2409f
equal deleted inserted replaced
16808:644fc45c7292 16809:8ca51a846576