src/Pure/pattern.ML
changeset 18595 a52907967bae
parent 18182 786d83044780
child 18940 d8e12bf337a3