src/Pure/pattern.ML
changeset 70538 fc9ba6fe367f
parent 70443 a21a96eda033
child 80910 406a85a25189
equal deleted inserted replaced
70537:17160e0a60b6 70538:fc9ba6fe367f