--- a/src/HOL/HOL.thy Wed May 27 21:02:44 2020 +0200
+++ b/src/HOL/HOL.thy Sat May 30 08:50:18 2020 +0000
@@ -1200,6 +1200,9 @@
simproc_setup defined_Ex ("\<exists>x. P x") = \<open>K Quantifier1.rearrange_Ex\<close>
simproc_setup defined_All ("\<forall>x. P x") = \<open>K Quantifier1.rearrange_All\<close>
+simproc_setup defined_all("\<And>x. PROP P x") = \<open>K Quantifier1.rearrange_all\<close>
+
+declare [[simproc del: defined_all]]
text \<open>Simproc for proving \<open>(y = x) \<equiv> False\<close> from premise \<open>\<not> (x = y)\<close>:\<close>
--- a/src/HOL/Library/Quantified_Premise_Simproc.thy Wed May 27 21:02:44 2020 +0200
+++ b/src/HOL/Library/Quantified_Premise_Simproc.thy Sat May 30 08:50:18 2020 +0000
@@ -4,6 +4,6 @@
imports Main
begin
-simproc_setup defined_all ("\<And>x. PROP P x") = \<open>K Quantifier1.rearrange_all\<close>
+declare [[simproc add: defined_all]]
end