src/Pure/pattern.ML
changeset 18260 5597cfcecd49
parent 18182 786d83044780
child 18940 d8e12bf337a3
equal deleted inserted replaced
18259:7b14579c58f2 18260:5597cfcecd49