[isabelle] Re: beginner question: why isn't my lemma applied?
On Saturday 01 October 2005 03:35, Andrew Pimlott wrote:
> lemma samekeys:
> "haskey (ps @ (k,v) # qs) k' = haskey (ps @ (k,v') # qs) k'";
> lemma "haskey (ps @ (k, v) # qs) k' --> haskey (ps @ (k, v') # qs) k'";
> -- ???
maybe someone else is going to write more about the simplifier, but the
following proof should solve your goal:
apply (subst samekeys)
This archive was generated by a fusion of
Pipermail (Mailman edition) and