hiding

Stream: general

[Reid Barton]

I imported tactic.ring to handle an identity and now as a result I have a lemma pow_two in the root namespace which conflicts with my own lemma pow_two, which I use about a dozen times in various proofs.
Is there a way to hide imported identifiers?