src/Pure/more_pattern.ML
changeset 70690 8518a750f7bb
parent 70443 a21a96eda033
child 74525 c960bfcb91db
equal deleted inserted replaced
70689:67360d50ebb3 70690:8518a750f7bb