install simproc but deactivate by default
authorhaftmann
Sat, 30 May 2020 08:50:18 +0000
changeset 72141 3867734b9a40
parent 72140 8357ee06ade1
child 72142 3956d85e8e81
install simproc but deactivate by default
src/HOL/HOL.thy
src/HOL/Library/Quantified_Premise_Simproc.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>
 
--- 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