[isabelle-dev] Is theorem Pair_inject in Product_Type still considered legacy or duplicate?
bulwahn at in.tum.de
Tue Oct 16 18:12:57 CEST 2012
in the changeset e8400e31528a of the Isabelle repository, you moved the
theorem Pair_inject in the Product_Type theory into a section called
"Legacy theorem bindings and duplicates".
In my current development, I rely on the theorem Pair_inject, and it is
the most suitable rule for my purpose.
Why was it considered legacy or a duplicate? Does this still hold at the
NB: At the current tip d7917ec16288, I cannot find any duplicate theorem
More information about the isabelle-dev