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.


	Makarius





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.