Re: [isabelle] discarding an assumption
>> where I've previously proved "discard_assumption" as
>> [| ?x ; ?y |] ==> ?y
> 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;
awesome, it seems i can just go
apply(thin_tac "blah") to make "blah" disappear from the assumptions!
> You say "Isabelle certainly warns about it" but I don't get such a warning,
> what does it say?
ah i just looked again and noticed i was doing (for some unknown reason):
lemma discard_assumption: "[| ?x ; ?y |] ==> ?y"
which produced the message:
[Isabelle] ### Goal statement contains unbound schematic variable(s): ?y, ?x
Which is what I was seeing as i was skipping through all my definitions
up to the main proof i'm working on.
Replacing them with x and y made it go away. However now I don't need
it anymore, anyway :)
This archive was generated by a fusion of
Pipermail (Mailman edition) and