--- a/src/HOL/HOL.thy Tue Oct 10 22:18:58 2017 +0100
+++ b/src/HOL/HOL.thy Mon Oct 09 19:10:47 2017 +0200
@@ -1574,6 +1574,14 @@
subsection \<open>Other simple lemmas and lemma duplicates\<close>
+lemma all_cong: "(\<And>x. Q x \<Longrightarrow> P x = P' x) \<Longrightarrow>
+ (ALL x. Q x \<longrightarrow> P x) = (ALL x. Q x \<longrightarrow> P' x)"
+ by auto
+
+lemma ex_cong: "(\<And>x. Q x \<Longrightarrow> P x = P' x) \<Longrightarrow>
+ (EX x. Q x \<and> P x) = (EX x. Q x \<and> P' x)"
+ by auto
+
lemma ex1_eq [iff]: "\<exists>!x. x = t" "\<exists>!x. t = x"
by blast+