src/Pure/pattern.ML
changeset 69729 4591221824f6
parent 69575 f77cc54f6d47
child 70443 a21a96eda033
equal deleted inserted replaced
69728:20bc1d26c932 69729:4591221824f6