# HG changeset patch
# User berghofe
# Date 908984435 -7200
# Node ID 5fc697ad232b789a1691df128886ec4e035e5429
# Parent  b4f2e281a9073781748b433a1559a117cfef1eaf
Added theorem prod_induct (needed for rep_datatype).

diff -r b4f2e281a907 -r 5fc697ad232b 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";