src/Pure/pattern.ML
changeset 5840 e2d2b896c717
parent 4820 8f6dbbd8d497
child 6539 2e7d2fba9f6c
equal deleted inserted replaced
5839:3ad1364bbb4b 5840:e2d2b896c717