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.
Lukas
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
