src/Pure/pattern.ML
changeset 16510 606d919ad3c3
parent 15797 a63605582573
child 16651 40b96a501773
equal deleted inserted replaced
16509:20f4c6a950f7 16510:606d919ad3c3