src/Pure/Proof/extraction.ML
changeset 80792 1cbdba868710
parent 80590 505f97165f52
child 81534 c32ebdcbe8ca