# HG changeset patch
# User blanchet
# Date 1335308261 -7200
# Node ID a8989fe9a3a5296eae1db928c64abf60b4705b84
# Parent  19b914b7ac2398ca8d1c99cb37329980d437f400
added "no_atp"s for extremely prolific, useless facts for ATPs

diff -r 19b914b7ac23 -r a8989fe9a3a5 src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Tue Apr 24 23:22:40 2012 +0200
+++ b/src/HOL/Product_Type.thy	Wed Apr 25 00:57:41 2012 +0200
@@ -379,7 +379,7 @@
 lemma cond_split_eta: "(!!x y. f x y = g (x, y)) ==> (%(x, y). f x y) = g"
   by (simp add: split_eta)
 
-lemma split_paired_all: "(!!x. PROP P x) == (!!a b. PROP P (a, b))"
+lemma split_paired_all [no_atp]: "(!!x. PROP P x) == (!!a b. PROP P (a, b))"
 proof
   fix a b
   assume "!!x. PROP P x"
@@ -425,14 +425,14 @@
   Classical.map_cs (fn cs => cs addSbefore ("split_all_tac", split_all_tac))
 *}
 
-lemma split_paired_All [simp]: "(ALL x. P x) = (ALL a b. P (a, b))"
+lemma split_paired_All [simp, no_atp]: "(ALL x. P x) = (ALL a b. P (a, b))"
   -- {* @{text "[iff]"} is not a good idea because it makes @{text blast} loop *}
   by fast
 
-lemma split_paired_Ex [simp]: "(EX x. P x) = (EX a b. P (a, b))"
+lemma split_paired_Ex [simp, no_atp]: "(EX x. P x) = (EX a b. P (a, b))"
   by fast
 
-lemma split_paired_The: "(THE x. P x) = (THE (a, b). P (a, b))"
+lemma split_paired_The [no_atp]: "(THE x. P x) = (THE (a, b). P (a, b))"
   -- {* Can't be added to simpset: loops! *}
   by (simp add: split_eta)
 
@@ -970,11 +970,11 @@
   -- {* Suggested by Pierre Chartier *}
   by blast
 
-lemma split_paired_Ball_Sigma [simp,no_atp]:
+lemma split_paired_Ball_Sigma [simp, no_atp]:
     "(ALL z: Sigma A B. P z) = (ALL x:A. ALL y: B x. P(x,y))"
   by blast
 
-lemma split_paired_Bex_Sigma [simp,no_atp]:
+lemma split_paired_Bex_Sigma [simp, no_atp]:
     "(EX z: Sigma A B. P z) = (EX x:A. EX y: B x. P(x,y))"
   by blast