Re: [isabelle] difference between "using" versus auto simp:
On Wed, 2 Feb 2011, Christian Urban wrote:
If you use "using", then Isar will add the lemma to the context, but
will fix the type variables in the theorem. That usually makes the lemma
More precisely, Isar does nothing more than adding the facts to the
"using" slot of the proof state. It is then up to the subsequent proof
method to make sense of it. For semi-automated methods like simp, auto,
blast etc. this means to insert the facts into the goal state and proceed
as usual. This effectively means that type variables cannot be
instantiated under most circumstances.
It is one of the many pitfalls of implicit polymorphism (or the lack
thereof) in certain situations.
This archive was generated by a fusion of
Pipermail (Mailman edition) and