Re: [isabelle] Announcing Isabelle2013-2

Le Fri, 06 Dec 2013 12:00:51 +0100, Makarius <makarius at> a écrit:

Isabelle2013-2 is now available.

I don't know if it's on purpose or not, at least surprising, an example of what may be returned by Sledgehammer:

    proof -
      have "t1 ≅ t2 ⟶ ω (t1 ∖ c) ≅ ω (t2 ∖ c)"
        using eqt rec by auto

There is no show/thus.

With this case, the goal was:

    "¬ t1 ≅ t2 ∨ ω (t1 ∖ c) ≅ ω (t2 ∖ c)"

I just added

    thus "¬ t1 ≅ t2 ∨ ω (t1 ∖ c) ≅ ω (t2 ∖ c)" by simp

… which it forgets.

The similar happens from time to time.

“Syntactic sugar causes cancer of the semi-colons.” [1]
“Structured Programming supports the law of the excluded muddle.” [1]
[1]: Epigrams on Programming — Alan J. — P. Yale University

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