# HG changeset patch
# User haftmann
# Date 1590828618 0
# Node ID 3867734b9a40f0bee9b0d24e9f526f1b68f6601c
# Parent  8357ee06ade15619fff97fbe65867b8db42053c2
install simproc but deactivate by default

diff -r 8357ee06ade1 -r 3867734b9a40 src/HOL/HOL.thy
--- 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>
 
diff -r 8357ee06ade1 -r 3867734b9a40 src/HOL/Library/Quantified_Premise_Simproc.thy
--- 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