# HG changeset patch
# User bulwahn
# Date 1336480263 -7200
# Node ID 4cf901b1089ac01325ee7eb5418460dca276e20e
# Parent  e389889da7df255d2e7df5679dd67bb513e78410
specialised fact in the Record theory should not be appear in proofs discovered by sledgehammer

diff -r e389889da7df -r 4cf901b1089a src/HOL/Record.thy
--- a/src/HOL/Record.thy	Mon May 07 14:50:49 2012 +0200
+++ b/src/HOL/Record.thy	Tue May 08 14:31:03 2012 +0200
@@ -400,7 +400,7 @@
 lemma refl_conj_eq: "Q = R \<Longrightarrow> P \<and> Q \<longleftrightarrow> P \<and> R"
   by simp
 
-lemma iso_tuple_UNIV_I: "x \<in> UNIV \<equiv> True"
+lemma iso_tuple_UNIV_I [no_atp]: "x \<in> UNIV \<equiv> True"
   by simp
 
 lemma iso_tuple_True_simp: "(True \<Longrightarrow> PROP P) \<equiv> PROP P"