src/Pure/pattern.ML
changeset 606 d5b322b33afb
parent 63 b1349b598560
child 678 6151b7f3b606