specialised fact in the Record theory should not be appear in proofs discovered by sledgehammer
authorbulwahn
Tue May 08 14:31:03 2012 +0200 (2012-05-08)
changeset 478934cf901b1089a
parent 47892 e389889da7df
child 47894 2c6454643be6
specialised fact in the Record theory should not be appear in proofs discovered by sledgehammer
src/HOL/Record.thy
     1.1 --- a/src/HOL/Record.thy	Mon May 07 14:50:49 2012 +0200
     1.2 +++ b/src/HOL/Record.thy	Tue May 08 14:31:03 2012 +0200
     1.3 @@ -400,7 +400,7 @@
     1.4  lemma refl_conj_eq: "Q = R \<Longrightarrow> P \<and> Q \<longleftrightarrow> P \<and> R"
     1.5    by simp
     1.6  
     1.7 -lemma iso_tuple_UNIV_I: "x \<in> UNIV \<equiv> True"
     1.8 +lemma iso_tuple_UNIV_I [no_atp]: "x \<in> UNIV \<equiv> True"
     1.9    by simp
    1.10  
    1.11  lemma iso_tuple_True_simp: "(True \<Longrightarrow> PROP P) \<equiv> PROP P"