src/Pure/pattern.ML
changeset 3864 e0ce3d4ec47d
parent 2792 6c17c5ec3d8b
child 4667 6328d427a339