src/Pure/more_pattern.ML
changeset 76692 98880b2430ea
parent 74525 c960bfcb91db
child 79242 b0774e7d1949
equal deleted inserted replaced
76691:0c6aa6c27ba4 76692:98880b2430ea