src/Pure/tactic.ML
changeset 8927 1cf815412d78
parent 8129 29e239c7b8c2
child 8977 dd8bc754a072