[isabelle] discarding an assumption



Is it possible to delete an assumption from the current subgoal?  While
unnecessary, I sometimes find this useful while proving in proof general
if the list of assumptions gets too big.  Maybe this makes the proof
space smaller while using the automatic methods too?  I've been doing

apply(erule_tac ?x="blah" in discard_assumption)

where I've previously proved "discard_assumption" as

[| ?x ; ?y |] ==> ?y

but I'm assuming this is a bad idea.  Isabelle certainly warns about it.
Is there a better way?


thanks





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.