[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

Previous message (by thread): [isabelle-dev] Is theorem Pair_inject in Product_Type still considered legacy or duplicate?
Next message (by thread): [isabelle-dev] Is theorem Pair_inject in Product_Type still considered legacy or duplicate?
Messages sorted by: [ date ] [ thread ] [ subject ] [ author ]

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]

Jasmin

Previous message (by thread): [isabelle-dev] Is theorem Pair_inject in Product_Type still considered legacy or duplicate?
Next message (by thread): [isabelle-dev] Is theorem Pair_inject in Product_Type still considered legacy or duplicate?
Messages sorted by: [ date ] [ thread ] [ subject ] [ author ]

More information about the isabelle-dev mailing list