src/Pure/Pure.thy

--- a/src/Pure/Pure.thy	Tue Mar 03 15:51:57 2020 +0100
+++ b/src/Pure/Pure.thy	Mon Mar 02 14:58:37 2020 +0000
@@ -1432,6 +1432,10 @@
 lemma swap_params:
   "(\<And>x y. PROP P x y) \<equiv> (\<And>y x. PROP P x y)" ..
 
+lemma equal_allI:
+  \<open>(\<And>x. PROP P x) \<equiv> (\<And>x. PROP Q x)\<close> if \<open>\<And>x. PROP P x \<equiv> PROP Q x\<close>
+  by (simp only: that)
+
 
 subsection \<open>Meta-level conjunction\<close>