[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?
This archive was generated by a fusion of
Pipermail (Mailman edition) and