# HG changeset patch
# User haftmann
# Date 1583263584 0
# Node ID bae868febc5361f4d8447b44b746c7bde935c9a2
# Parent  7807d828a0613aeeca51c9ffff0034c9c8485090
library theory for extractions of equations x = t into premises

diff -r 7807d828a061 -r bae868febc53 src/HOL/Library/Quantified_Premise_Simproc.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Quantified_Premise_Simproc.thy	Tue Mar 03 19:26:24 2020 +0000
@@ -0,0 +1,9 @@
+(* Author: Florian Haftmann, TU München *)
+
+theory Quantified_Premise_Simproc
+  imports Main
+begin
+
+simproc_setup defined_forall ("\<And>x. PROP P x") = \<open>K Quantifier1.rearrange_All\<close>
+
+end
diff -r 7807d828a061 -r bae868febc53 src/HOL/ROOT
--- a/src/HOL/ROOT	Tue Mar 03 19:26:23 2020 +0000
+++ b/src/HOL/ROOT	Tue Mar 03 19:26:24 2020 +0000
@@ -52,6 +52,7 @@
     OptionalSugar
     (*prototypic tools*)
     Predicate_Compile_Quickcheck
+    Quantified_Premise_Simproc
     (*legacy tools*)
     Old_Datatype
     Old_Recdef