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