src/Pure/tactic.ML
changeset 8657 b9475dad85ed
parent 8129 29e239c7b8c2
child 8977 dd8bc754a072
equal deleted inserted replaced
8656:1062572b5b37 8657:b9475dad85ed