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