Re: [isabelle] rule Unifies With Chained Facts?
On Sun, 3 Apr 2011, Rafal Kolanski wrote:
I still remain surprised whenever I have to replace "by blast" with "by
- blast". As for fastsimp, force and metis... I just don't remember.
"by blast" and "by - blast" should be always the same.
Since blast is a "simple method" it first uses "insert" to dump the facts
into the goal state and then tries its luck on the result.
This archive was generated by a fusion of
Pipermail (Mailman edition) and