src/Pure/pattern.ML
changeset 70842 c5caf81aa523
parent 70443 a21a96eda033
child 80910 406a85a25189
equal deleted inserted replaced
70841:3d8953224f33 70842:c5caf81aa523