[isabelle-dev] Is theorem Pair_inject in Product_Type still considered legacy or duplicate?

Jasmin Christian Blanchette jasmin.blanchette at gmail.com
Tue Oct 16 19:13:59 CEST 2012

Am 16.10.2012 um 18:12 schrieb Lukas Bulwahn:

> NB: At the current tip d7917ec16288, I cannot find any duplicate theorem for Pair_inject.

    prod.inject[THEN iffD1, THEN conjE]


More information about the isabelle-dev mailing list