src/Pure/pattern.ML
changeset 863 67692db44c70
parent 678 6151b7f3b606
child 1029 27808dabf4af