author | berghofe |
Wed, 21 Oct 1998 17:40:35 +0200 | |
changeset 5715 | 5fc697ad232b |
parent 5714 | b4f2e281a907 |
child 5716 | a3d2a6b6693e |
src/HOL/Prod.ML | file | annotate | diff | comparison | revisions |
--- a/src/HOL/Prod.ML Wed Oct 21 17:38:47 1998 +0200 +++ b/src/HOL/Prod.ML Wed Oct 21 17:40:35 1998 +0200 @@ -97,6 +97,9 @@ Addsimps [split_paired_All]; (* AddIffs is not a good idea because it makes Blast_tac loop *) +bind_thm ("prod_induct", + allI RS (allI RS (split_paired_All RS iffD2)) RS spec); + Goal "(? x. P x) = (? a b. P(a,b))"; by (Fast_tac 1); qed "split_paired_Ex";