src/Pure/more_pattern.ML
changeset 68041 d45b78cb86cf
parent 67010 cf56dd6f3ad1
child 70443 a21a96eda033
equal deleted inserted replaced
68040:362baebe25a5 68041:d45b78cb86cf