src/Pure/pattern.ML
changeset 12596 34265656f0b4
parent 12527 d6c91bc3e49c
child 12781 f76180d14819
equal deleted inserted replaced
12595:0480d02221b8 12596:34265656f0b4