src/HOL/Prod.ML

--- 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";