src/Pure/pattern.ML
changeset 16608 4f8d7b83c7e2
parent 15797 a63605582573
child 16651 40b96a501773
equal deleted inserted replaced
16607:81e687c63e29 16608:4f8d7b83c7e2