equal
deleted
inserted
replaced
398 by (simp add: isomorphic_tuple_intro [OF _ _ reflexive] tuple_iso_tuple_def) |
398 by (simp add: isomorphic_tuple_intro [OF _ _ reflexive] tuple_iso_tuple_def) |
399 |
399 |
400 lemma refl_conj_eq: "Q = R \<Longrightarrow> P \<and> Q \<longleftrightarrow> P \<and> R" |
400 lemma refl_conj_eq: "Q = R \<Longrightarrow> P \<and> Q \<longleftrightarrow> P \<and> R" |
401 by simp |
401 by simp |
402 |
402 |
403 lemma iso_tuple_UNIV_I: "x \<in> UNIV \<equiv> True" |
403 lemma iso_tuple_UNIV_I [no_atp]: "x \<in> UNIV \<equiv> True" |
404 by simp |
404 by simp |
405 |
405 |
406 lemma iso_tuple_True_simp: "(True \<Longrightarrow> PROP P) \<equiv> PROP P" |
406 lemma iso_tuple_True_simp: "(True \<Longrightarrow> PROP P) \<equiv> PROP P" |
407 by simp |
407 by simp |
408 |
408 |