changeset 71914 | 3867734b9a40 |
parent 71886 | 4f4695757980 |
--- 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