src/Pure/pattern.ML
changeset 2840 7e03e61612b0
parent 2792 6c17c5ec3d8b
child 4667 6328d427a339