Re: [isabelle] discarding an assumption

Dave Cunningham wrote:
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?



I can't see why it is a bad idea, except for the fact that your


is in fact thin_rl, already in Isabelle.

In fact the tactic thin_tac does exactly what you have done

tactic.ML:fun thin_tac s = eres_inst_tac [("V",s)] thin_rl;

You say "Isabelle certainly warns about it" but I don't get such a warning, what does it say?



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