src/Pure/tactic.ML
changeset 82733 8b537e1af2ec
parent 74282 c2ee8d993d6a