src/Pure/tactic.ML
changeset 79074 7f24c5be57bd
parent 74282 c2ee8d993d6a