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

Lukas Bulwahn bulwahn at in.tum.de
Tue Oct 16 18:12:57 CEST 2012

Hi Florian,

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 
current tip?

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


More information about the isabelle-dev mailing list