Re: [isabelle] Announcing Isabelle2013-2



Le Fri, 06 Dec 2013 12:00:51 +0100, Makarius <makarius at sketis.net> 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
    qed

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.