src/Pure/pattern.ML
changeset 3776 38f8ec304b95
parent 2792 6c17c5ec3d8b
child 4667 6328d427a339