src/Pure/more_pattern.ML
changeset 59047 8d7cec9b861d
parent 59027 f9bee88c5912
child 59095 3100a7b1c092
equal deleted inserted replaced
59046:db5a718e8c09 59047:8d7cec9b861d