Use thin_tac to throw away assumptions that you don't need in order to prove your subgoal.
Thin_tac needs a scheme for knowing, which assumption it should use.
The first matching assumption will be deleted.

Examples:

lemma "⟦P t0;∀t. P t⟧ ⟹ P t0"
apply (thin_tac "∀x. P x")
goal (1 subgoal):
 1. P t0 ⟹ P t0

forget all assumptions: use a always matching scheme as often as possible
apply (thin_tac "?x")+