src/Pure/pattern.ML
changeset 18260 5597cfcecd49
parent 18182 786d83044780
child 18940 d8e12bf337a3