changeset 47893 | 4cf901b1089a |
parent 46950 | d0181abdbdac |
child 48891 | c0eafbd55de3 |
--- 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"