Re: [isabelle] Type annotations



PS Correction: In the latest version

lemma fails:
"[| ALL n1 n2. (k :: obj => obj) n1 = (k :: obj => obj) n2 --> n1 = n2;
     k (x1::obj) = k (x2::obj) |] ==> (x1::obj) = (x2::obj)"
by simp

actually works, because the infinite descent is stopped.

Tobias





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