# 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 ("\x. P x") = \K Quantifier1.rearrange_Ex\ simproc_setup defined_All ("\x. P x") = \K Quantifier1.rearrange_All\ +simproc_setup defined_all("\x. PROP P x") = \K Quantifier1.rearrange_all\ + +declare [[simproc del: defined_all]] text \Simproc for proving \(y = x) \ False\ from premise \\ (x = y)\:\ 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 ("\x. PROP P x") = \K Quantifier1.rearrange_all\ +declare [[simproc add: defined_all]] end